let M1, M2 be Matrix of ExtREAL; :: thesis: ( len M1 = len M2 & ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) implies (SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2) )
assume A1: ( len M1 = len M2 & ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) ) ; :: thesis: (SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)
A2: len (Sum M1) = len M1 by Def5
.= len (Sum M2) by A1, Def5 ;
then reconsider p1 = Sum M1, p2 = Sum M2 as Element of (len (Sum M1)) -tuples_on ExtREAL by FINSEQ_2:92;

C0: now :: thesis: not -infty in rng (Sum M1)

assume -infty in rng (Sum M1) ; :: thesis: contradiction
then consider i being Nat such that
C1: ( i in dom (Sum M1) & (Sum M1) . i = -infty ) by FINSEQ_2:10;
i in Seg (len (Sum M1)) by C1, FINSEQ_1:def 3;
then i in Seg (len M1) by Def5;
then i in dom M1 by FINSEQ_1:def 3;
then C2: not -infty in rng (M1 . i) by A1;
(Sum M1) . i = Sum (M1 . i) by C1, Def5;
then ex j being Nat st
( j in dom (M1 . i) & (M1 . i) . j = -infty ) by C1, Th17;
hence contradiction by C2, FUNCT_1:3; :: thesis: verum

end;

A3: now :: thesis: not -infty in rng (Sum M2)

assume -infty in rng (Sum M2) ; :: thesis: contradiction
then consider i being Nat such that
C1: ( i in dom (Sum M2) & (Sum M2) . i = -infty ) by FINSEQ_2:10;
i in Seg (len (Sum M2)) by C1, FINSEQ_1:def 3;
then i in Seg (len M2) by Def5;
then i in dom M2 by FINSEQ_1:def 3;
then C2: not -infty in rng (M2 . i) by A1;
(Sum M2) . i = Sum (M2 . i) by C1, Def5;
then ex j being Nat st
( j in dom (M2 . i) & (M2 . i) . j = -infty ) by C1, Th17;
hence contradiction by C2, FUNCT_1:3; :: thesis: verum

end;

A4: dom (Sum M1) = dom (Sum M2) by A2, FINSEQ_3:29;
Sum (M1 ^^ M2) = (Sum M1) + (Sum M2) by A1, Th24;
hence (SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2) by A3, C0, A4, Th18; :: thesis: verum