let MR be Matrix of REAL ; :: thesis: SumAll MR = Sum (Mx2FinS MR)

per cases ( len MR = 0 or len MR > 0 ) ;

suppose A1: len MR = 0 ; :: thesis: SumAll MR = Sum (Mx2FinS MR)

hence Sum (Mx2FinS MR) = 0 by Def5, RVSUM_1:102
.= SumAll MR by A1, MATRPROB:23 ;
:: thesis: verum

end;

suppose len MR > 0 ; :: thesis: SumAll MR = Sum (Mx2FinS MR)

then consider p being FinSequence of REAL * such that
A2: Mx2FinS MR = p . (len MR) and
A3: ( len p = len MR & p . 1 = MR . 1 & ( for k being Element of NAT st k >= 1 & k < len MR holds
p . (k + 1) = (p . k) ^ (MR . (k + 1)) ) ) by Def5;
thus SumAll MR = Sum (Mx2FinS MR) by A2, A3, Th38; :: thesis: verum

end;

end;