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