let M be empty-yielding with_line_sum=1 Matrix of REAL; :: thesis: SumAll M = len M
set n = len M;
A1: ( len (Sum M) = len M & ( for i being Nat st i in dom (Sum M) holds
(Sum M) . i = 1 ) )

proof

thus len (Sum M) = len M by Def1; :: thesis: for i being Nat st i in dom (Sum M) holds
(Sum M) . i = 1

hereby :: thesis: verum

let i be Nat; :: thesis: ( i in dom (Sum M) implies (Sum M) . i = 1 )
assume A2: i in dom (Sum M) ; :: thesis: (Sum M) . i = 1
then i in Seg (len (Sum M)) by FINSEQ_1:def 3;
then i in Seg (len M) by Def1;
then i in dom M by FINSEQ_1:def 3;
then Sum (M . i) = 1 by Def9;
hence (Sum M) . i = 1 by A2, Def1; :: thesis: verum

end;

end;

len M > 0 by Th54;
then Sum M = (len M) |-> jj by A1, Th1;
hence SumAll M = (len M) * 1 by RVSUM_1:80
.= len M ;
:: thesis: verum