src/HOL/Probability/Sigma_Algebra.thy

     using measurable_sets[OF f `A \<in> sets N`] \<Omega> by blast
   finally show "f -` A \<inter> space (restrict_space M \<Omega>) \<in> sets (restrict_space M \<Omega>)" .
 qed
 
 lemma measurable_restrict_space2:
-  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
+  "\<Omega> \<inter> space N \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
     f \<in> measurable M (restrict_space N \<Omega>)"
-  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
+  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff Pi_Int[symmetric])
 
 end