consider M being MidSp;
set D = the carrier of M;
set k = (n + 1) + 1;
set C = ((n + 1) + 1) -tuples_on the carrier of M;
reconsider one = 1 as Nat of n + 1 by Th24;
deffunc H₁( Element of ((n + 1) + 1) -tuples_on the carrier of M) -> Element of the carrier of M = $1 . one;
consider R being Function of (((n + 1) + 1) -tuples_on the carrier of M),the carrier of M such that
A1: for p being Element of ((n + 1) + 1) -tuples_on the carrier of M holds R . p = H₁(p) from FUNCT_2:sch 4();
reconsider R = R as Function of ((n + 2) -tuples_on the carrier of M),the carrier of M ;
reconsider RA = ReperAlgebraStr(# the carrier of M,the MIDPOINT of M,R #) as non empty MidSp-like ReperAlgebraStr of n + 2 by Lm3;
A2: 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)
A3: *' b,q = (<*b*> ^ q) . one by A1
.= b by FINSEQ_1:58 ;
*' a,p = (<*a*> ^ p) . one by A1
.= a by FINSEQ_1:58 ;
hence a @ (*' b,q) = b @ (*' a,p) by A3; :: thesis: verum

end;

take RA ; :: thesis: RA is being_invariance
thus RA is being_invariance by A2, Def5; :: thesis: verum