let m be Nat; :: thesis: for M being Matrix of m, 0 ,ExtREAL holds SumAll M = 0
let M be Matrix of m, 0 ,ExtREAL; :: 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 Th21; :: thesis: verum

end;

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

then len M > 0 by MATRIX_0:def 2;
then reconsider k = len (Sum M) as non zero Nat by Def5;
reconsider Z = 0. as R_eal ;
for k being Nat st k in dom (Sum M) holds
(Sum M) . k = 0

proof

len M = len (Sum M) by Def5;
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
then M . k in rng M by A2, FUNCT_1:def 3;
then M . k = <*> ExtREAL by MATRIX_0:def 2;
hence (Sum M) . k = 0 by A3, Def5, EXTREAL1:7; :: thesis: verum

end;

end;

then Sum M = k |-> 0. by MATRPROB:1;
then SumAll M = (len (Sum M)) * Z by Th20;
hence SumAll M = 0 ; :: thesis: verum

end;

end;