:: deftheorem defines Z_Lin RLVECT_X:def 3 :
for RS being RealLinearSpace
for f being FinSequence of RS holds Z_Lin f = { (Sum g) where g is len b₂ -element FinSequence of RS : ex a being INT -valued len b₂ -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) } ;