:: deftheorem Def5 defines (#) CONVEX4:def 5 :
for V being non empty CLSStruct
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,COMPLEX
for b₄ being FinSequence of the carrier 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) ) ) );