let m be Nat; :: thesis: for V1 being free finite-rank Z_Module
for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1
let V1 be free finite-rank Z_Module; :: 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 MATRLIN:def 6;
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, MATRLIN:def 6
.= 0. V1 by A2, RLVECT_1:43 ; :: thesis: verum
end;
hence Sum (Sum M) = 0. V1 by MATRLIN:11; :: thesis: verum