let m be Nat; :: thesis: for M being Matrix of m, 0 ,REAL holds SumAll M = 0
let M be Matrix of m, 0 ,REAL; :: thesis: SumAll M = 0

per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: SumAll M = 0

then len M = 0 by MATRIX_0:def 2;
hence SumAll M = 0 by Th23; :: thesis: verum

end;

suppose A1: m > 0 ; :: thesis: SumAll M = 0

( len (Sum M) > 0 & ( for k being Nat st k in dom (Sum M) holds
(Sum M) . k = 0 ) )

proof

len M > 0 by A1, MATRIX_0:def 2;
hence len (Sum M) > 0 by Def1; :: thesis: for k being Nat st k in dom (Sum M) holds
(Sum M) . k = 0
len M = len (Sum M) by Def1;
then A2: dom M = dom (Sum M) by FINSEQ_3:29;

hereby :: thesis: verum

let k be Nat; :: thesis: ( k in dom (Sum M) implies (Sum M) . k = 0 )
assume A3: k in dom (Sum M) ; :: thesis: (Sum M) . k = 0
M . k in rng M by A2, A3, FUNCT_1:def 3;
then len (M . k) = 0 by MATRIX_0:def 2;
then A4: M . k = <*> REAL ;
thus (Sum M) . k = Sum (M . k) by A3, Def1
.= 0 by A4, RVSUM_1:72 ; :: thesis: verum

end;

end;

hence SumAll M = Sum ((len (Sum M)) |-> 0) by Th1, Lm4
.= (len (Sum M)) * 0 by RVSUM_1:80
.= 0 ;
:: thesis: verum

end;

end;