let M1, M2 be Matrix of REAL; :: thesis: ( len M1 = len M2 implies (SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2) )
assume A1: len M1 = len M2 ; :: thesis: (SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)
len (Sum M1) = len M1 by Def1
.= len (Sum M2) by A1, Def1 ;
then reconsider p1 = Sum M1, p2 = Sum M2 as Element of (len (Sum M1)) -tuples_on REAL by FINSEQ_2:92;
thus (SumAll M1) + (SumAll M2) = Sum (p1 + p2) by RVSUM_1:89
.= SumAll (M1 ^^ M2) by Th26 ; :: thesis: verum