:: deftheorem Def3 defines |-- RLAFFIN3:def 3 :
for V being RealLinearSpace
for A being Subset of V
for x being set
for b₄ being Function of V,R^1 holds
( b₄ = |-- (A,x) iff for v being VECTOR of V holds b₄ . v = (v |-- A) . x );