src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Product_Type.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -1137,6 +1137,10 @@
 lemma Times_Int_Times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   by auto
 
+lemma image_paired_Times:
+   "(\<lambda>(x,y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
+  by auto
+
 lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
   by (auto simp add: set_eq_iff)