src/HOL/Library/Formal_Power_Series.thy
changeset 61943 7fba644ed827
parent 61804 67381557cee8
child 61969 e01015e49041
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -3108,7 +3108,7 @@
     1.4      setsum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}"  (is "?l = ?r")
     1.5  proof -
     1.6    let ?S = "{(k::nat, m::nat). k + m \<le> n}"
     1.7 -  have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
     1.8 +  have s: "?S \<subseteq> {0..n} \<times> {0..n}" by (auto simp add: subset_eq)
     1.9    have f: "finite {(k::nat, m::nat). k + m \<le> n}"
    1.10      apply (rule finite_subset[OF s])
    1.11      apply auto