let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K

for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

let V1 be finite-dimensional VectSp of K; :: thesis: for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

let M1, M2 be Matrix of the carrier of V1; :: thesis: (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

reconsider m = min ((len M1),(len M2)) as Element of NAT by ORDINAL1:def 12;

A1: Seg m = (Seg (len M1)) /\ (Seg (len M2)) by FINSEQ_2:2

.= (Seg (len M1)) /\ (dom M2) by FINSEQ_1:def 3

.= (dom M1) /\ (dom M2) by FINSEQ_1:def 3

.= dom (M1 ^^ M2) by PRE_POLY:def 4

.= Seg (len (M1 ^^ M2)) by FINSEQ_1:def 3 ;

A2: len ((Sum M1) + (Sum M2)) = min ((len (Sum M1)),(len (Sum M2))) by FINSEQ_2:71

.= min ((len M1),(len (Sum M2))) by Def6

.= min ((len M1),(len M2)) by Def6

.= len (M1 ^^ M2) by A1, FINSEQ_1:6

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

A3: dom ((Sum M1) + (Sum M2)) = Seg (len ((Sum M1) + (Sum M2))) by FINSEQ_1:def 3;

for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

let V1 be finite-dimensional VectSp of K; :: thesis: for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

let M1, M2 be Matrix of the carrier of V1; :: thesis: (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)

reconsider m = min ((len M1),(len M2)) as Element of NAT by ORDINAL1:def 12;

A1: Seg m = (Seg (len M1)) /\ (Seg (len M2)) by FINSEQ_2:2

.= (Seg (len M1)) /\ (dom M2) by FINSEQ_1:def 3

.= (dom M1) /\ (dom M2) by FINSEQ_1:def 3

.= dom (M1 ^^ M2) by PRE_POLY:def 4

.= Seg (len (M1 ^^ M2)) by FINSEQ_1:def 3 ;

A2: len ((Sum M1) + (Sum M2)) = min ((len (Sum M1)),(len (Sum M2))) by FINSEQ_2:71

.= min ((len M1),(len (Sum M2))) by Def6

.= min ((len M1),(len M2)) by Def6

.= len (M1 ^^ M2) by A1, FINSEQ_1:6

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

A3: dom ((Sum M1) + (Sum M2)) = Seg (len ((Sum M1) + (Sum M2))) by FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom ((Sum M1) + (Sum M2)) holds

((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i

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

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

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

then A5: i in dom (Sum (M1 ^^ M2)) by A2, A3, FINSEQ_1:def 3;

i in Seg (len (M1 ^^ M2)) by A2, A3, A4, Def6;

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

then A7: i in (dom M1) /\ (dom M2) by PRE_POLY:def 4;

then A8: i in dom M1 by XBOOLE_0:def 4;

A9: i in dom M2 by A7, XBOOLE_0:def 4;

reconsider m1 = M1 . i, m2 = M2 . i as FinSequence ;

A10: (M1 /. i) ^ (M2 /. i) = m1 ^ (M2 /. i) by A8, PARTFUN1:def 6

.= m1 ^ m2 by A9, PARTFUN1:def 6

.= (M1 ^^ M2) . i by A6, PRE_POLY:def 4

.= (M1 ^^ M2) /. i by A6, PARTFUN1:def 6 ;

i in Seg (len M2) by A9, FINSEQ_1:def 3;

then i in Seg (len (Sum M2)) by Def6;

then A11: i in dom (Sum M2) by FINSEQ_1:def 3;

then A12: (Sum M2) /. i = (Sum M2) . i by PARTFUN1:def 6;

i in Seg (len M1) by A8, FINSEQ_1:def 3;

then i in Seg (len (Sum M1)) by Def6;

then A13: i in dom (Sum M1) by FINSEQ_1:def 3;

then (Sum M1) /. i = (Sum M1) . i by PARTFUN1:def 6;

hence ((Sum M1) + (Sum M2)) . i = ((Sum M1) /. i) + ((Sum M2) /. i) by A4, A12, FUNCOP_1:22

.= (Sum (M1 /. i)) + ((Sum M2) /. i) by A13, Def6

.= (Sum (M1 /. i)) + (Sum (M2 /. i)) by A11, Def6

.= Sum ((M1 ^^ M2) /. i) by A10, RLVECT_1:41

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

.= (Sum (M1 ^^ M2)) . i by A5, PARTFUN1:def 6 ;

:: thesis: verum

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

then A5: i in dom (Sum (M1 ^^ M2)) by A2, A3, FINSEQ_1:def 3;

i in Seg (len (M1 ^^ M2)) by A2, A3, A4, Def6;

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

then A7: i in (dom M1) /\ (dom M2) by PRE_POLY:def 4;

then A8: i in dom M1 by XBOOLE_0:def 4;

A9: i in dom M2 by A7, XBOOLE_0:def 4;

reconsider m1 = M1 . i, m2 = M2 . i as FinSequence ;

A10: (M1 /. i) ^ (M2 /. i) = m1 ^ (M2 /. i) by A8, PARTFUN1:def 6

.= m1 ^ m2 by A9, PARTFUN1:def 6

.= (M1 ^^ M2) . i by A6, PRE_POLY:def 4

.= (M1 ^^ M2) /. i by A6, PARTFUN1:def 6 ;

i in Seg (len M2) by A9, FINSEQ_1:def 3;

then i in Seg (len (Sum M2)) by Def6;

then A11: i in dom (Sum M2) by FINSEQ_1:def 3;

then A12: (Sum M2) /. i = (Sum M2) . i by PARTFUN1:def 6;

i in Seg (len M1) by A8, FINSEQ_1:def 3;

then i in Seg (len (Sum M1)) by Def6;

then A13: i in dom (Sum M1) by FINSEQ_1:def 3;

then (Sum M1) /. i = (Sum M1) . i by PARTFUN1:def 6;

hence ((Sum M1) + (Sum M2)) . i = ((Sum M1) /. i) + ((Sum M2) /. i) by A4, A12, FUNCOP_1:22

.= (Sum (M1 /. i)) + ((Sum M2) /. i) by A13, Def6

.= (Sum (M1 /. i)) + (Sum (M2 /. i)) by A11, Def6

.= Sum ((M1 ^^ M2) /. i) by A10, RLVECT_1:41

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

.= (Sum (M1 ^^ M2)) . i by A5, PARTFUN1:def 6 ;

:: thesis: verum