let L be non empty addLoopStr ; :: thesis: for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)
let F, G be FinSequence of the carrier of L * ; :: thesis: Sum (F ^ G) = (Sum F) ^ (Sum G)
A1: dom (Sum F) = dom F by Th2;
A2: dom (Sum G) = dom G by Th2;
A3: len ((Sum F) ^ (Sum G)) = (len (Sum F)) + (len (Sum G)) by FINSEQ_1:22
.= (len F) + (len (Sum G)) by A1, FINSEQ_3:29
.= (len F) + (len G) by A2, FINSEQ_3:29
.= len (F ^ G) by FINSEQ_1:22 ;
then A4: dom ((Sum F) ^ (Sum G)) = dom (F ^ G) by FINSEQ_3:29;
A5: len (Sum F) = len F by A1, FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom (F ^ G) holds
((Sum F) ^ (Sum G)) /. i = Sum ((F ^ G) /. i)

let i be Nat; :: thesis: ( i in dom (F ^ G) implies ((Sum F) ^ (Sum G)) /. b₁ = Sum ((F ^ G) /. b₁) )
assume A6: i in dom (F ^ G) ; :: thesis: ((Sum F) ^ (Sum G)) /. b₁ = Sum ((F ^ G) /. b₁)

per cases ( i in dom F or ex n being Nat st
( n in dom G & i = (len F) + n ) ) by A6, FINSEQ_1:25;

suppose A7: i in dom F ; :: thesis: ((Sum F) ^ (Sum G)) /. b₁ = Sum ((F ^ G) /. b₁)

thus ((Sum F) ^ (Sum G)) /. i = ((Sum F) ^ (Sum G)) . i by A4, A6, PARTFUN1:def 6
.= (Sum F) . i by A1, A7, FINSEQ_1:def 7
.= (Sum F) /. i by A1, A7, PARTFUN1:def 6
.= Sum (F /. i) by A1, A7, MATRLIN:def 6
.= Sum ((F ^ G) /. i) by A7, FINSEQ_4:68 ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom G & i = (len F) + n ) ; :: thesis: ((Sum F) ^ (Sum G)) /. b₁ = Sum ((F ^ G) /. b₁)

then consider n being Nat such that
A8: n in dom G and
A9: i = (len F) + n ;
thus ((Sum F) ^ (Sum G)) /. i = ((Sum F) ^ (Sum G)) . i by A4, A6, PARTFUN1:def 6
.= (Sum G) . n by A2, A5, A8, A9, FINSEQ_1:def 7
.= (Sum G) /. n by A2, A8, PARTFUN1:def 6
.= Sum (G /. n) by A2, A8, MATRLIN:def 6
.= Sum ((F ^ G) /. i) by A8, A9, FINSEQ_4:69 ; :: thesis: verum

end;

end;

end;

hence Sum (F ^ G) = (Sum F) ^ (Sum G) by A3, A4, MATRLIN:def 6; :: thesis: verum