let L be Z_Lattice; :: thesis: for v being Vector of (DivisibleMod L) holds SumSc (v,(ZeroLC (DivisibleMod L))) = 0. F_Real
let v be Vector of (DivisibleMod L); :: thesis: SumSc (v,(ZeroLC (DivisibleMod L))) = 0. F_Real
consider F being FinSequence of (DivisibleMod L) such that
A1: ( F is one-to-one & rng F = Carrier (ZeroLC (DivisibleMod L)) & SumSc (v,(ZeroLC (DivisibleMod L))) = Sum (ScFS (v,(ZeroLC (DivisibleMod L)),F)) ) by defSumScDM;
F = {} by A1, VECTSP_6:def 3;
then len (ScFS (v,(ZeroLC (DivisibleMod L)),F)) = 0 by defScFSDM;
hence SumSc (v,(ZeroLC (DivisibleMod L))) = 0. F_Real by A1, RLVECT_1:75; :: thesis: verum