970 proof (induct j) |
970 proof (induct j) |
971 case 0 from Rf Rg show ?case by (simp add: Pi_def) |
971 case 0 from Rf Rg show ?case by (simp add: Pi_def) |
972 next |
972 next |
973 case (Suc j) |
973 case (Suc j) |
974 have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R" |
974 have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R" |
975 using Suc by (auto intro!: funcset_mem [OF Rg]) arith |
975 using Suc by (auto intro!: funcset_mem [OF Rg]) |
976 have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R" |
976 have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R" |
977 using Suc by (auto intro!: funcset_mem [OF Rg]) arith |
977 using Suc by (auto intro!: funcset_mem [OF Rg]) |
978 have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R" |
978 have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R" |
979 using Suc by (auto intro!: funcset_mem [OF Rf]) |
979 using Suc by (auto intro!: funcset_mem [OF Rf]) |
980 have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R" |
980 have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R" |
981 using Suc by (auto intro!: funcset_mem [OF Rg]) arith |
981 using Suc by (auto intro!: funcset_mem [OF Rg]) |
982 have R11: "g 0 \<in> carrier R" |
982 have R11: "g 0 \<in> carrier R" |
983 using Suc by (auto intro!: funcset_mem [OF Rg]) |
983 using Suc by (auto intro!: funcset_mem [OF Rg]) |
984 from Suc show ?case |
984 from Suc show ?case |
985 by (simp cong: finsum_cong add: Suc_diff_le a_ac |
985 by (simp cong: finsum_cong add: Suc_diff_le a_ac |
986 Pi_def R6 R8 R9 R10 R11) |
986 Pi_def R6 R8 R9 R10 R11) |