theorem Th24: :: MIDSP_3:24

for n being Nat
for RAS being ReperAlgebra of n
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 (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v