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:72
.= SumAll MR by A1, MATRPROB:23 ;
:: thesis: verum
end;
suppose len MR > 0 ; :: thesis: SumAll MR = Sum (Mx2FinS MR)
then ex p being FinSequence of REAL * st
( Mx2FinS MR = p . (len MR) & len p = len MR & p . 1 = MR . 1 & ( for k being Nat st k >= 1 & k < len MR holds
p . (k + 1) = (p . k) ^ (MR . (k + 1)) ) ) by Def5;
hence SumAll MR = Sum (Mx2FinS MR) by Th38; :: thesis: verum
end;
end;