:: deftheorem defines being_invariance MIDSP_3:def 3 :
for n being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS is being_invariance iff for a, b being Point of RAS
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p)) );