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 Th15;
A2: dom (Sum G) = dom G by Th15;
A3: len (Sum F) = len F by A1, FINSEQ_3:31;
A4: len ((Sum F) ^ (Sum G)) = (len (Sum F)) + (len (Sum G)) by FINSEQ_1:35
.= (len F) + (len (Sum G)) by A1, FINSEQ_3:31
.= (len F) + (len G) by A2, FINSEQ_3:31
.= len (F ^ G) by FINSEQ_1:35 ;
then A5: dom ((Sum F) ^ (Sum G)) = dom (F ^ G) by FINSEQ_3:31;

now

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:38;

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 A5, A6, PARTFUN1:def 8
.= (Sum F) . i by A1, A7, FINSEQ_1:def 7
.= (Sum F) /. i by A1, A7, PARTFUN1:def 8
.= Sum (F /. i) by A1, A7, MATRLIN:def 8
.= Sum ((F ^ G) /. i) by A7, FINSEQ_4:83 ; :: 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 A5, A6, PARTFUN1:def 8
.= (Sum G) . n by A2, A3, A8, A9, FINSEQ_1:def 7
.= (Sum G) /. n by A2, A8, PARTFUN1:def 8
.= Sum (G /. n) by A2, A8, MATRLIN:def 8
.= Sum ((F ^ G) /. i) by A8, A9, FINSEQ_4:84 ; :: thesis: verum

end;

end;

end;

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