theorem Th14: :: MIDSP_3:14

for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for x, y being Tuple of (n + 1),W st ( for m being Nat of n holds x . m = y . m ) holds
x = y