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_1:def 3;
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_1:def 3;
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:31;

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 5;
then len (M . k) = 0 by MATRIX_1:def 3;
then B4: M . k = <*> REAL ;
thus (Sum M) . k = Sum (M . k) by A3, Def1
.= 0 by B4, RVSUM_1:102 ; :: thesis: verum

end;

end;

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

end;

end;