let M1, M2 be Matrix of REAL ; :: thesis: (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
reconsider M = min (len M1),(len M2) as Element of NAT by FINSEQ_2:1;
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 MATRLIN:def 2
.= Seg (len (M1 ^^ M2)) by FINSEQ_1:def 3 ;
A2: len ((Sum M1) + (Sum M2)) = len (addreal .: (Sum M1),(Sum M2)) by RVSUM_1:def 4
.= min (len (Sum M1)),(len (Sum M2)) by FINSEQ_2:85
.= min (len M1),(len (Sum M2)) by Def1
.= min (len M1),(len M2) by Def1
.= len (M1 ^^ M2) by A1, FINSEQ_1:8
.= len (Sum (M1 ^^ M2)) by Def1 ;
X: dom ((Sum M1) + (Sum M2)) = Seg (len ((Sum M1) + (Sum M2))) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom ((Sum M1) + (Sum M2)) implies ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i )
assume A3: i in dom ((Sum M1) + (Sum M2)) ; :: thesis: ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i
then A4: i in dom (addreal .: (Sum M1),(Sum M2)) by RVSUM_1:def 4;
A5: i in dom (Sum (M1 ^^ M2)) by A2, A3, X, FINSEQ_1:def 3;
i in Seg (len (M1 ^^ M2)) by A2, A3, Def1, X;
then A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3;
then i in (dom M1) /\ (dom M2) by MATRLIN:def 2;
then ( i in dom M1 & i in dom M2 ) by XBOOLE_0:def 4;
then ( i in Seg (len M1) & i in Seg (len M2) ) by FINSEQ_1:def 3;
then ( i in Seg (len (Sum M1)) & i in Seg (len (Sum M2)) ) by Def1;
then A7: ( i in dom (Sum M1) & i in dom (Sum M2) ) by FINSEQ_1:def 3;
A8: (M1 . i) ^ (M2 . i) = (M1 ^^ M2) . i by A6, MATRLIN:def 2;
thus ((Sum M1) + (Sum M2)) . i = (addreal .: (Sum M1),(Sum M2)) . i by RVSUM_1:def 4
.= addreal . ((Sum M1) . i),((Sum M2) . i) by A4, FUNCOP_1:28
.= ((Sum M1) . i) + ((Sum M2) . i) by BINOP_2:def 9
.= (Sum (M1 . i)) + ((Sum M2) . i) by A7, Def1
.= (Sum (M1 . i)) + (Sum (M2 . i)) by A7, Def1
.= Sum ((M1 ^^ M2) . i) by A8, RVSUM_1:105
.= (Sum (M1 ^^ M2)) . i by A5, Def1 ; :: thesis: verum

end;

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