let n be Nat; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS holds
( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: thesis: for W being ATLAS of RAS holds
( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
let W be ATLAS of RAS; :: thesis: ( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
A1: ( ( for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ) implies RAS is being_invariance )

proof

assume A2: for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ; :: thesis: RAS is being_invariance
let a be Point of RAS; :: according to MIDSP_3:def 3 :: thesis: for 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))
let b be Point of RAS; :: thesis: 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))
let p, q be Tuple of (n + 1),RAS; :: thesis: ( ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) implies a @ (*' (b,q)) = b @ (*' (a,p)) )
A3: W . (a,(*' (a,((a,(W . (a,p))) . W)))) = Phi (a,(W . (a,p)))
.= Phi (b,(W . (a,p))) by A2
.= W . (b,(*' (b,((b,(W . (a,p))) . W)))) ;
assume A4: for m being Nat of n holds a @ (q . m) = b @ (p . m) ; :: thesis: a @ (*' (b,q)) = b @ (*' (a,p))

A5: now :: thesis: for m being Nat of n holds (W . (a,p)) . m = (W . (b,q)) . m

let m be Nat of n; :: thesis: (W . (a,p)) . m = (W . (b,q)) . m
a @ (q . m) = b @ (p . m) by A4;
then A6: W . (a,(p . m)) = W . (b,(q . m)) by MIDSP_2:33;
thus (W . (a,p)) . m = W . (a,(p . m)) by Def9
.= (W . (b,q)) . m by A6, Def9 ; :: thesis: verum

end;

W . (a,(*' (a,p))) = W . (a,(*' (a,((a,(W . (a,p))) . W)))) by Th15
.= W . (b,(*' (b,((b,(W . (b,q))) . W)))) by A5, A3, Th14
.= W . (b,(*' (b,q))) by Th15 ;
hence a @ (*' (b,q)) = b @ (*' (a,p)) by MIDSP_2:33; :: thesis: verum

end;

now :: thesis: ( RAS is being_invariance implies for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )

assume A7: RAS is being_invariance ; :: thesis: for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let a, b be Point of RAS; :: thesis: for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let x be Tuple of (n + 1),W; :: thesis: Phi (a,x) = Phi (b,x)
set p = (a,x) . W;
set q = (b,x) . W;
A8: W . (a,((a,x) . W)) = x by Th15
.= W . (b,((b,x) . W)) by Th15 ;

now :: thesis: for m being Nat of n holds a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m)

let m be Nat of n; :: thesis: a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m)
W . (a,(((a,x) . W) . m)) = (W . (a,((a,x) . W))) . m by Def9
.= W . (b,(((b,x) . W) . m)) by A8, Def9 ;
hence a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m) by MIDSP_2:33; :: thesis: verum

end;

then a @ (*' (b,((b,x) . W))) = b @ (*' (a,((a,x) . W))) by A7;
hence Phi (a,x) = Phi (b,x) by MIDSP_2:33; :: thesis: verum

end;

hence ( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ) by A1; :: thesis: verum