let n be Element of NAT ; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr of 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 of 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: now

assume A2: 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;
A3: W . a,(a,x . W) = x by Th17
.= W . b,(b,x . W) by Th17 ;

now

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 Def12
.= W . b,((b,x . W) . m) by A3, Def12 ;
hence a @ ((b,x . W) . m) = b @ ((a,x . W) . m) by MIDSP_2:39; :: thesis: verum

end;

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

end;

( ( 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 A4: 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 5 :: 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) )
assume A5: for m being Nat of n holds a @ (q . m) = b @ (p . m) ; :: thesis: a @ (*' b,q) = b @ (*' a,p)
a @ (*' b,q) = b @ (*' a,p)

proof

A6: now

let m be Nat of n; :: thesis: (W . a,p) . m = (W . b,q) . m
a @ (q . m) = b @ (p . m) by A5;
then A7: W . a,(p . m) = W . b,(q . m) by MIDSP_2:39;
thus (W . a,p) . m = W . a,(p . m) by Def12
.= (W . b,q) . m by A7, Def12 ; :: thesis: verum

end;

A8: W . a,(*' a,(a,(W . a,p) . W)) = Phi a,(W . a,p)
.= Phi b,(W . a,p) by A4
.= W . b,(*' b,(b,(W . a,p) . W)) ;
W . a,(*' a,p) = W . a,(*' a,(a,(W . a,p) . W)) by Th17
.= W . b,(*' b,(b,(W . b,q) . W)) by A6, A8, Th16
.= W . b,(*' b,q) by Th17 ;
hence a @ (*' b,q) = b @ (*' a,p) by MIDSP_2:39; :: thesis: verum

end;

hence a @ (*' b,q) = b @ (*' a,p) ; :: 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