let k, m, n 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: dom (Sum (M1 ^ M2)) = Seg (len (Sum (M1 ^ M2))) by FINSEQ_1:def 3;

.= (len M1) + (len M2) by FINSEQ_1:22

.= (len (Sum M1)) + (len M2) by Def6

.= (len (Sum M1)) + (len (Sum M2)) by Def6

.= len ((Sum M1) ^ (Sum M2)) by FINSEQ_1:22 ;

hence Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) by A2, FINSEQ_2:9; :: thesis: verum

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

len (Sum (M1 ^ M2)) =
len (M1 ^ M2)
by Def6
(Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i

let i be Nat; :: thesis: ( i in dom (Sum (M1 ^ M2)) implies (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i )

assume A3: i in dom (Sum (M1 ^ M2)) ; :: thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i

then i in Seg (len (M1 ^ M2)) by A1, Def6;

then A4: i in dom (M1 ^ M2) by FINSEQ_1:def 3;

end;assume A3: i in dom (Sum (M1 ^ M2)) ; :: thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i

then i in Seg (len (M1 ^ M2)) by A1, Def6;

then A4: i in dom (M1 ^ M2) by FINSEQ_1:def 3;

now :: thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . iend;

hence
(Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i
; :: thesis: verumper cases
( i in dom M1 or ex n being Nat st

( n in dom M2 & i = (len M1) + n ) ) by A4, FINSEQ_1:25;

end;

( n in dom M2 & i = (len M1) + n ) ) by A4, FINSEQ_1:25;

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

len M1 = len (Sum M1)
by Def6;

then A6: dom M1 = dom (Sum M1) by FINSEQ_3:29;

thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def 6

.= Sum ((M1 ^ M2) /. i) by A3, Def6

.= Sum (M1 /. i) by A5, FINSEQ_4:68

.= (Sum M1) /. i by A5, A6, Def6

.= (Sum M1) . i by A5, A6, PARTFUN1:def 6

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

end;then A6: dom M1 = dom (Sum M1) by FINSEQ_3:29;

thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def 6

.= Sum ((M1 ^ M2) /. i) by A3, Def6

.= Sum (M1 /. i) by A5, FINSEQ_4:68

.= (Sum M1) /. i by A5, A6, Def6

.= (Sum M1) . i by A5, A6, PARTFUN1:def 6

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

suppose A7:
ex n being Nat st

( n in dom M2 & i = (len M1) + n ) ; :: thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i

( n in dom M2 & i = (len M1) + n ) ; :: thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i

A8:
len M1 = len (Sum M1)
by Def6;

len M2 = len (Sum M2) by Def6;

then A9: dom M2 = dom (Sum M2) by FINSEQ_3:29;

consider n being Nat such that

A10: n in dom M2 and

A11: i = (len M1) + n by A7;

thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def 6

.= Sum ((M1 ^ M2) /. i) by A3, Def6

.= Sum (M2 /. n) by A10, A11, FINSEQ_4:69

.= (Sum M2) /. n by A10, A9, Def6

.= (Sum M2) . n by A10, A9, PARTFUN1:def 6

.= ((Sum M1) ^ (Sum M2)) . i by A10, A11, A8, A9, FINSEQ_1:def 7 ; :: thesis: verum

end;len M2 = len (Sum M2) by Def6;

then A9: dom M2 = dom (Sum M2) by FINSEQ_3:29;

consider n being Nat such that

A10: n in dom M2 and

A11: i = (len M1) + n by A7;

thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def 6

.= Sum ((M1 ^ M2) /. i) by A3, Def6

.= Sum (M2 /. n) by A10, A11, FINSEQ_4:69

.= (Sum M2) /. n by A10, A9, Def6

.= (Sum M2) . n by A10, A9, PARTFUN1:def 6

.= ((Sum M1) ^ (Sum M2)) . i by A10, A11, A8, A9, FINSEQ_1:def 7 ; :: thesis: verum

.= (len M1) + (len M2) by FINSEQ_1:22

.= (len (Sum M1)) + (len M2) by Def6

.= (len (Sum M1)) + (len (Sum M2)) by Def6

.= len ((Sum M1) ^ (Sum M2)) by FINSEQ_1:22 ;

hence Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) by A2, FINSEQ_2:9; :: thesis: verum