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 )

for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ) by A1; :: thesis: verum

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))

.= 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;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

W . (a,(*' (a,p))) =
W . (a,(*' (a,((a,(W . (a,p))) . W))))
by Th15
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;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

.= 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

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) )

hence
( RAS is being_invariance iff for a, b being Point of RASfor 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 ;

hence Phi (a,x) = Phi (b,x) by MIDSP_2:33; :: thesis: verum

end;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)

then
a @ (*' (b,((b,x) . W))) = b @ (*' (a,((a,x) . W)))
by A7;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;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

hence Phi (a,x) = Phi (b,x) by MIDSP_2:33; :: thesis: verum

for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ) by A1; :: thesis: verum