theorem :: MIDSP_3:17

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