equal
deleted
inserted
replaced
509 { fix A |
509 { fix A |
510 have "?p ` (A \<inter> space M) \<subseteq> |
510 have "?p ` (A \<inter> space M) \<subseteq> |
511 (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)" |
511 (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)" |
512 by auto |
512 by auto |
513 hence "finite (?p ` (A \<inter> space M))" |
513 hence "finite (?p ` (A \<inter> space M))" |
514 by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) } |
514 by (rule finite_subset) auto } |
515 note this[intro, simp] |
515 note this[intro, simp] |
516 |
516 |
517 { fix x assume "x \<in> space M" |
517 { fix x assume "x \<in> space M" |
518 have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto |
518 have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto |
519 moreover { |
519 moreover { |