let L be Z_Lattice; :: thesis: for v, u being Vector of L
for l being Linear_Combination of {u} holds SumSc (v,l) = <;v,((l . u) * u);>
let v, u be Vector of L; :: 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 VECTSP_6:def 4, ZFMISC_1:33;
suppose Carrier l = {} ; :: thesis: SumSc (v,l) = <;v,((l . u) * u);>
then A2: l = ZeroLC L by VECTSP_6:def 3;
hence SumSc (v,l) = 0. F_Real by LmSumSc11
.= <;v,(0. L);> by ZMODLAT1:12
.= <;v,((0. INT.Ring) * u);> by VECTSP_1:14
.= <;v,((l . u) * u);> by A2, VECTSP_6:3 ;
:: thesis: verum
end;
suppose Carrier l = {u} ; :: thesis: SumSc (v,l) = <;v,((l . u) * u);>
then consider F being FinSequence of L such that
A3: ( F is one-to-one & rng F = {u} & SumSc (v,l) = Sum (ScFS (v,l,F)) ) by defSumSc;
F = <*u*> by A3, FINSEQ_3:97;
then ScFS (v,l,F) = <*<;v,((l . u) * u);>*> by ThScFS3;
hence SumSc (v,l) = <;v,((l . u) * u);> by A3, RLVECT_1:44; :: thesis: verum
end;
end;