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

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

hence
Sum (Sum M) = 0. V1
by Th11; :: thesis: verum
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;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