--- a/src/HOL/Library/FuncSet.thy Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/Library/FuncSet.thy Wed Oct 28 11:42:31 2009 +0000
@@ -101,6 +101,19 @@
lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
by auto
+lemma prod_final:
+ assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
+ shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
+proof (rule Pi_I)
+ fix z
+ assume z: "z \<in> A"
+ have "f z = (fst (f z), snd (f z))"
+ by simp
+ also have "... \<in> B z \<times> C z"
+ by (metis SigmaI PiE o_apply 1 2 z)
+ finally show "f z \<in> B z \<times> C z" .
+qed
+
subsection{*Composition With a Restricted Domain: @{term compose}*}