:: deftheorem Def5 defines (#) VECTSP_6:def 5 :
for GF being non empty addLoopStr
for V being non empty ModuleStr over GF
for F being FinSequence of the carrier of V
for f being Function of V,GF
for b₅ being FinSequence of V holds
( b₅ = f (#) F iff ( len b₅ = len F & ( for i being Nat st i in dom b₅ holds
b₅ . i = (f . (F /. i)) * (F /. i) ) ) );