:: deftheorem Def8 defines . MIDSP_3:def 8 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for a being Point of RAS
for x being Tuple of (n + 1),W
for b₆ being Tuple of (n + 1),RAS holds
( b₆ = (a,x) . W iff for m being Nat of n holds b₆ . m = (a,(x . m)) . W );