for RS being RealLinearSpace
for f being non empty FinSequence of RS
for g, h being FinSequence of RS
for s being INT -valued FinSequence st rng g c= Z_Lin f & len g = len s & len g = len h & ( for i being Nat st i in Seg (len g) holds
h /. i = (s . i) * (g /. i) ) holds
Sum h in Z_Lin f