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

for l being Linear_Combination of {} the carrier of L holds SumSc (v,l) = 0. F_Real

let v be Vector of L; :: thesis: for l being Linear_Combination of {} the carrier of L holds SumSc (v,l) = 0. F_Real

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

l = ZeroLC L by VECTSP_6:6;

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

for l being Linear_Combination of {} the carrier of L holds SumSc (v,l) = 0. F_Real

let v be Vector of L; :: thesis: for l being Linear_Combination of {} the carrier of L holds SumSc (v,l) = 0. F_Real

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

l = ZeroLC L by VECTSP_6:6;

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