let m be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1
let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1
let V1 be finite-dimensional VectSp of K; :: thesis: for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1
let M be Matrix of m + 1, 0 , the carrier of V1; :: thesis: Sum (Sum M) = 0. V1
for k being Nat st k in dom (Sum M) holds
(Sum M) /. k = 0. V1

proof

let k be Nat; :: thesis: ( k in dom (Sum M) implies (Sum M) /. k = 0. V1 )
assume A1: k in dom (Sum M) ; :: thesis: (Sum M) /. k = 0. V1
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
len M = len (Sum M) by Def6;
then dom M = dom (Sum M) by FINSEQ_3:29;
then M /. k1 in rng M by A1, PARTFUN2:2;
then len (M /. k) = 0 by MATRIX_0:def 2;
then A2: M /. k = <*> the carrier of V1 ;
thus (Sum M) /. k = Sum (M /. k) by A1, Def6
.= 0. V1 by A2, RLVECT_1:43 ; :: thesis: verum

end;

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