let n, k, m be Nat; :: thesis: for K being Field
for V being VectSp of K
for M1 being Matrix of n,k,the carrier of V
for M2 being Matrix of m,k,the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let K be Field; :: thesis: for V being VectSp of K
for M1 being Matrix of n,k,the carrier of V
for M2 being Matrix of m,k,the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let V be VectSp of K; :: thesis: for M1 being Matrix of n,k,the carrier of V
for M2 being Matrix of m,k,the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let M1 be Matrix of n,k,the carrier of V; :: thesis: for M2 being Matrix of m,k,the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
let M2 be Matrix of m,k,the carrier of V; :: thesis: Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
A1: len (Sum (M1 ^ M2)) = len (M1 ^ M2) by Def8
.= (len M1) + (len M2) by FINSEQ_1:35
.= (len (Sum M1)) + (len M2) by Def8
.= (len (Sum M1)) + (len (Sum M2)) by Def8
.= len ((Sum M1) ^ (Sum M2)) by FINSEQ_1:35 ;
X: dom (Sum (M1 ^ M2)) = Seg (len (Sum (M1 ^ M2))) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom (Sum (M1 ^ M2)) implies (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i )
assume A2: i in dom (Sum (M1 ^ M2)) ; :: thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i
then A3: i in dom (Sum (M1 ^ M2)) ;
i in Seg (len (M1 ^ M2)) by A2, Def8, X;
then A4: i in dom (M1 ^ M2) by FINSEQ_1:def 3;

now

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

suppose A6: i in dom M1 ; :: thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i

len M1 = len (Sum M1) by Def8;
then A7: dom M1 = dom (Sum M1) by FINSEQ_3:31;
thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def 8
.= Sum ((M1 ^ M2) /. i) by A3, Def8
.= Sum (M1 /. i) by A6, FINSEQ_4:83
.= (Sum M1) /. i by A6, A7, Def8
.= (Sum M1) . i by A6, A7, PARTFUN1:def 8
.= ((Sum M1) ^ (Sum M2)) . i by A6, A7, 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)) . i = ((Sum M1) ^ (Sum M2)) . i

then consider n being Nat such that
A8: ( n in dom M2 & i = (len M1) + n ) ;
A9: len M1 = len (Sum M1) by Def8;
len M2 = len (Sum M2) by Def8;
then A10: dom M2 = dom (Sum M2) by FINSEQ_3:31;
thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def 8
.= Sum ((M1 ^ M2) /. i) by A3, Def8
.= Sum (M2 /. n) by A8, FINSEQ_4:84
.= (Sum M2) /. n by A8, A10, Def8
.= (Sum M2) . n by A8, A10, PARTFUN1:def 8
.= ((Sum M1) ^ (Sum M2)) . i by A8, A9, A10, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i ; :: thesis: verum

end;

hence Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) by A1, FINSEQ_2:10; :: thesis: verum