let L be Z_Lattice; :: thesis: for v being Vector of (DivisibleMod L)

for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds

SumSc (v,l) = 0. F_Real

let v be Vector of (DivisibleMod L); :: thesis: for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds

SumSc (v,l) = 0. F_Real

let l be Linear_Combination of DivisibleMod L; :: thesis: ( Carrier l = {} implies SumSc (v,l) = 0. F_Real )

assume A1: Carrier l = {} ; :: thesis: SumSc (v,l) = 0. F_Real

l = ZeroLC (DivisibleMod L) by A1, VECTSP_6:def 3;

hence SumSc (v,l) = 0. F_Real by LmSumScDM11; :: thesis: verum

for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds

SumSc (v,l) = 0. F_Real

let v be Vector of (DivisibleMod L); :: thesis: for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds

SumSc (v,l) = 0. F_Real

let l be Linear_Combination of DivisibleMod L; :: thesis: ( Carrier l = {} implies SumSc (v,l) = 0. F_Real )

assume A1: Carrier l = {} ; :: thesis: SumSc (v,l) = 0. F_Real

l = ZeroLC (DivisibleMod L) by A1, VECTSP_6:def 3;

hence SumSc (v,l) = 0. F_Real by LmSumScDM11; :: thesis: verum