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