let L be Z_Lattice; :: thesis: for v being Vector of L holds SumSc (v,(ZeroLC L)) = 0. F_Real

let v be Vector of L; :: thesis: SumSc (v,(ZeroLC L)) = 0. F_Real

consider F being FinSequence of L such that

A1: ( F is one-to-one & rng F = Carrier (ZeroLC L) & SumSc (v,(ZeroLC L)) = Sum (ScFS (v,(ZeroLC L),F)) ) by defSumSc;

F = {} by A1, VECTSP_6:def 3;

then len (ScFS (v,(ZeroLC L),F)) = 0 by defScFS;

hence SumSc (v,(ZeroLC L)) = 0. F_Real by A1, RLVECT_1:75; :: thesis: verum

let v be Vector of L; :: thesis: SumSc (v,(ZeroLC L)) = 0. F_Real

consider F being FinSequence of L such that

A1: ( F is one-to-one & rng F = Carrier (ZeroLC L) & SumSc (v,(ZeroLC L)) = Sum (ScFS (v,(ZeroLC L),F)) ) by defSumSc;

F = {} by A1, VECTSP_6:def 3;

then len (ScFS (v,(ZeroLC L),F)) = 0 by defScFS;

hence SumSc (v,(ZeroLC L)) = 0. F_Real by A1, RLVECT_1:75; :: thesis: verum