theorem Th18: :: MIDSP_3:18

for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v holds
( *' (a,p) = b iff Phi (a,x) = v )