src/HOL/Algebra/FiniteProduct.thy
changeset 69313 b021008c5397
parent 68517 6b5f15387353
child 69895 6b03a8cf092d
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -576,7 +576,7 @@
     1.4    assumes
     1.5      "finite I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "pairwise (\<lambda>i j. disjnt (A i) (A j)) I"
     1.6      "\<And>i x. i \<in> I \<Longrightarrow> x \<in> A i \<Longrightarrow> g x \<in> carrier G"
     1.7 -shows "finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
     1.8 +shows "finprod G g (\<Union>(A ` I)) = finprod G (\<lambda>i. finprod G g (A i)) I"
     1.9    using assms
    1.10  proof (induction set: finite)
    1.11    case empty