theorem Th22: :: MIDSP_3:22

for n being Nat
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) by Def11, Th19;