let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K

for M being Matrix of the carrier of V1 st len M = 0 holds

Sum (Sum M) = 0. V1

let V1 be finite-dimensional VectSp of K; :: 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 Def6;

then Sum M = <*> the carrier of V1 ;

hence Sum (Sum M) = 0. V1 by RLVECT_1:43; :: thesis: verum

for M being Matrix of the carrier of V1 st len M = 0 holds

Sum (Sum M) = 0. V1

let V1 be finite-dimensional VectSp of K; :: 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 Def6;

then Sum M = <*> the carrier of V1 ;

hence Sum (Sum M) = 0. V1 by RLVECT_1:43; :: thesis: verum