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);>

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;

end;

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;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

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;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