theorem Th26: :: RLVECT_X:26

for RS being RealLinearSpace
for f being FinSequence of RS
for x being set holds
( x in Z_Lin f iff ex g being len b₂ -element FinSequence of RS ex a being INT -valued len b₂ -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) )