reconsider one1 = 1 as Nat of n + 1 by Th21;

set M = the MidSp;

set D = the carrier of the MidSp;

set k = (n + 1) + 1;

set C = ((n + 1) + 1) -tuples_on the carrier of the MidSp;

deffunc H_{1}( Element of ((n + 1) + 1) -tuples_on the carrier of the MidSp) -> Element of the carrier of the MidSp = $1 . one1;

consider R being Function of (((n + 1) + 1) -tuples_on the carrier of the MidSp), the carrier of the MidSp such that

A1: for p being Element of ((n + 1) + 1) -tuples_on the carrier of the MidSp holds R . p = H_{1}(p)
from FUNCT_2:sch 4();

reconsider R = R as Function of ((n + 2) -tuples_on the carrier of the MidSp), the carrier of the MidSp ;

reconsider RA = ReperAlgebraStr(# the carrier of the MidSp, the MIDPOINT of the MidSp,R #) as non empty MidSp-like ReperAlgebraStr over n + 2 by Lm3;

take RA ; :: thesis: RA is being_invariance

for a, b being Point of RA

for p, q being Tuple of (n + 1),RA st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds

a @ (*' (b,q)) = b @ (*' (a,p))

set M = the MidSp;

set D = the carrier of the MidSp;

set k = (n + 1) + 1;

set C = ((n + 1) + 1) -tuples_on the carrier of the MidSp;

deffunc H

consider R being Function of (((n + 1) + 1) -tuples_on the carrier of the MidSp), the carrier of the MidSp such that

A1: for p being Element of ((n + 1) + 1) -tuples_on the carrier of the MidSp holds R . p = H

reconsider R = R as Function of ((n + 2) -tuples_on the carrier of the MidSp), the carrier of the MidSp ;

reconsider RA = ReperAlgebraStr(# the carrier of the MidSp, the MIDPOINT of the MidSp,R #) as non empty MidSp-like ReperAlgebraStr over n + 2 by Lm3;

take RA ; :: thesis: RA is being_invariance

for a, b being Point of RA

for p, q being Tuple of (n + 1),RA st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds

a @ (*' (b,q)) = b @ (*' (a,p))

proof

hence
RA is being_invariance
; :: thesis: verum
let a, b be Point of RA; :: thesis: for p, q being Tuple of (n + 1),RA 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),RA; :: thesis: ( ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) implies a @ (*' (b,q)) = b @ (*' (a,p)) )

assume for m being Nat of n holds a @ (q . m) = b @ (p . m) ; :: thesis: a @ (*' (b,q)) = b @ (*' (a,p))

A2: *' (a,p) = (<*a*> ^ p) . one1 by A1

.= a by FINSEQ_1:41 ;

*' (b,q) = (<*b*> ^ q) . one1 by A1

.= b by FINSEQ_1:41 ;

hence a @ (*' (b,q)) = b @ (*' (a,p)) by A2; :: thesis: verum

end;a @ (*' (b,q)) = b @ (*' (a,p))

let p, q be Tuple of (n + 1),RA; :: thesis: ( ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) implies a @ (*' (b,q)) = b @ (*' (a,p)) )

assume for m being Nat of n holds a @ (q . m) = b @ (p . m) ; :: thesis: a @ (*' (b,q)) = b @ (*' (a,p))

A2: *' (a,p) = (<*a*> ^ p) . one1 by A1

.= a by FINSEQ_1:41 ;

*' (b,q) = (<*b*> ^ q) . one1 by A1

.= b by FINSEQ_1:41 ;

hence a @ (*' (b,q)) = b @ (*' (a,p)) by A2; :: thesis: verum