theorem :: MIDSP_3:16

for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for a being Point of RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds W . (a,((a,x) . W)) = x by Th15;