let L be Z_Lattice; :: thesis: for v, u being Vector of ()
for l being Linear_Combination of {u} holds SumSc (v,l) = () . (v,((l . u) * u))

let v, u be Vector of (); :: thesis: for l being Linear_Combination of {u} holds SumSc (v,l) = () . (v,((l . u) * u))
let l be Linear_Combination of {u}; :: thesis: SumSc (v,l) = () . (v,((l . u) * u))
per cases ( Carrier l = {} or Carrier l = {u} ) by ;
suppose Carrier l = {} ; :: thesis: SumSc (v,l) = () . (v,((l . u) * u))
then A2: l = ZeroLC () by VECTSP_6:def 3;
hence SumSc (v,l) = 0. F_Real by LmSumScDM11
.= () . (v,(0. ())) by ZMODLAT2:14
.= () . (v,(() * u)) by VECTSP_1:14
.= () . (v,((l . u) * u)) by ;
:: thesis: verum
end;
suppose Carrier l = {u} ; :: thesis: SumSc (v,l) = () . (v,((l . u) * u))
then consider F being FinSequence of () such that
A3: ( F is one-to-one & rng F = {u} & SumSc (v,l) = Sum (ScFS (v,l,F)) ) by defSumScDM;
F = <*u*> by ;
then ScFS (v,l,F) = <*(() . (v,((l . u) * u)))*> by ThScFSDM3;
hence SumSc (v,l) = () . (v,((l . u) * u)) by ; :: thesis: verum
end;
end;