let V1 be free finite-rank Z_Module; :: thesis: for M being Matrix of the carrier of V1 st len M = 0 holds
Sum (Sum M) = 0. V1
let M be Matrix of the carrier of V1; :: thesis: ( len M = 0 implies Sum (Sum M) = 0. V1 )
assume len M = 0 ; :: thesis: Sum (Sum M) = 0. V1
then len (Sum M) = 0 by MATRLIN:def 6;
then Sum M = <*> the carrier of V1 ;
hence Sum (Sum M) = 0. V1 by RLVECT_1:43; :: thesis: verum