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

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