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

proof

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;

hence RA is being_invariance ; :: thesis: verum