theorem Th9: :: MIDSP_3:9

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