let L be Z_Lattice; :: thesis: for v being Vector of L
for l being Linear_Combination of L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real
let v be Vector of L; :: thesis: for l being Linear_Combination of L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real
let l be Linear_Combination of L; :: thesis: ( Carrier l = {} implies SumSc (v,l) = 0. F_Real )
assume Carrier l = {} ; :: thesis: SumSc (v,l) = 0. F_Real
then l = ZeroLC L by VECTSP_6:def 3;
hence SumSc (v,l) = 0. F_Real by LmSumSc11; :: thesis: verum