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 H1( 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 = H1(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
; 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;
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;
( ( 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)
;
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;
verum
end;
hence
RA is being_invariance
; verum