let M be V3() 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