:: deftheorem Def12 defines Phi MIDSP_3:def 12 :
for n being Nat
for RAS being ReperAlgebra of n
for W being ATLAS of RAS
for x being Tuple of (n + 1),W
for b₅ being Vector of W holds
( b₅ = Phi x iff for a being Point of RAS holds b₅ = Phi (a,x) );