let n, m, k be Nat; :: thesis: for M1 being Matrix of n,k,ExtREAL
for M2 being Matrix of m,k,ExtREAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let M1 be Matrix of n,k,ExtREAL; :: thesis: for M2 being Matrix of m,k,ExtREAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let M2 be Matrix of m,k,ExtREAL; :: thesis: Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
A1: dom (Sum (M1 ^ M2)) = Seg (len (Sum (M1 ^ M2))) by FINSEQ_1:def 3;

A2: now :: thesis: for i being Nat st i in dom (Sum (M1 ^ M2)) holds
(Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i

let i be Nat; :: thesis: ( i in dom (Sum (M1 ^ M2)) implies (Sum (M1 ^ M2)) . b₁ = ((Sum M1) ^ (Sum M2)) . b₁ )
assume A3: i in dom (Sum (M1 ^ M2)) ; :: thesis: (Sum (M1 ^ M2)) . b₁ = ((Sum M1) ^ (Sum M2)) . b₁
then i in Seg (len (M1 ^ M2)) by A1, Def5;
then A4: i in dom (M1 ^ M2) by FINSEQ_1:def 3;
A8: ( len M1 = len (Sum M1) & len M2 = len (Sum M2) ) by Def5;
then A6: ( dom M1 = dom (Sum M1) & dom M2 = dom (Sum M2) ) by FINSEQ_3:29;

per cases ( i in dom M1 or ex n being Nat st
( n in dom M2 & i = (len M1) + n ) ) by A4, FINSEQ_1:25;

suppose A5: i in dom M1 ; :: thesis: (Sum (M1 ^ M2)) . b₁ = ((Sum M1) ^ (Sum M2)) . b₁

thus (Sum (M1 ^ M2)) . i = Sum ((M1 ^ M2) . i) by A3, Def5
.= Sum (M1 . i) by A5, FINSEQ_1:def 7
.= (Sum M1) . i by A5, A6, Def5
.= ((Sum M1) ^ (Sum M2)) . i by A5, A6, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

then consider n being Nat such that
A10: ( n in dom M2 & i = (len M1) + n ) ;
thus (Sum (M1 ^ M2)) . i = Sum ((M1 ^ M2) . i) by A3, Def5
.= Sum (M2 . n) by A10, FINSEQ_1:def 7
.= (Sum M2) . n by A10, A6, Def5
.= ((Sum M1) ^ (Sum M2)) . i by A10, A8, A6, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

len (Sum (M1 ^ M2)) = len (M1 ^ M2) by Def5
.= (len M1) + (len M2) by FINSEQ_1:22
.= (len (Sum M1)) + (len M2) by Def5
.= (len (Sum M1)) + (len (Sum M2)) by Def5
.= len ((Sum M1) ^ (Sum M2)) by FINSEQ_1:22 ;
hence Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) by A2, FINSEQ_2:9; :: thesis: verum