let K be Field; :: thesis: for V1 being finite-dimensional VectSp of finite-dimensional
for M being Matrix of st len M = 0 holds
Sum (Sum M) = 0. V1
let V1 be finite-dimensional VectSp of finite-dimensional ; :: thesis: for M being Matrix of st len M = 0 holds
Sum (Sum M) = 0. V1
let M be Matrix of ; :: 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 Def8;
then Sum M = <*> the carrier of V1 ;
hence Sum (Sum M) = 0. V1 by RLVECT_1:60; :: thesis: verum