let L be Z_Lattice; :: thesis: for v being Vector of (DivisibleMod L)
for l being Linear_Combination of {} the carrier of (DivisibleMod L) holds SumSc (v,l) = 0. F_Real
let v be Vector of (DivisibleMod L); :: thesis: for l being Linear_Combination of {} the carrier of (DivisibleMod L) holds SumSc (v,l) = 0. F_Real
let l be Linear_Combination of {} the carrier of (DivisibleMod L); :: thesis: SumSc (v,l) = 0. F_Real
l = ZeroLC (DivisibleMod L) by VECTSP_6:6;
hence SumSc (v,l) = 0. F_Real by LmSumScDM11; :: thesis: verum