let A be non empty set ; for f, g being Permutation of A
for R being Relation of [:A,A:] st f is_FormalIz_of R & g is_automorphism_of R holds
f \ g is_FormalIz_of R
let f, g be Permutation of A; for R being Relation of [:A,A:] st f is_FormalIz_of R & g is_automorphism_of R holds
f \ g is_FormalIz_of R
let R be Relation of [:A,A:]; ( f is_FormalIz_of R & g is_automorphism_of R implies f \ g is_FormalIz_of R )
assume that
A1:
for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R
and
A2:
for x, y, z, t being Element of A holds
( [[x,y],[z,t]] in R iff [[(g . x),(g . y)],[(g . z),(g . t)]] in R )
; TRANSGEO:def 2,TRANSGEO:def 3 f \ g is_FormalIz_of R
let x be Element of A; TRANSGEO:def 2 for y being Element of A holds [[x,y],[((f \ g) . x),((f \ g) . y)]] in R
let y be Element of A; [[x,y],[((f \ g) . x),((f \ g) . y)]] in R
A3:
[[((g ") . x),((g ") . y)],[(f . ((g ") . x)),(f . ((g ") . y))]] in R
by A1;
( g . ((g ") . x) = x & g . ((g ") . y) = y )
by Th2;
then
[[x,y],[(g . (f . ((g ") . x))),(g . (f . ((g ") . y)))]] in R
by A2, A3;
then
[[x,y],[((g * f) . ((g ") . x)),(g . (f . ((g ") . y)))]] in R
by FUNCT_2:15;
then
[[x,y],[((g * f) . ((g ") . x)),((g * f) . ((g ") . y))]] in R
by FUNCT_2:15;
then
[[x,y],[(((g * f) * (g ")) . x),((g * f) . ((g ") . y))]] in R
by FUNCT_2:15;
hence
[[x,y],[((f \ g) . x),((f \ g) . y)]] in R
by FUNCT_2:15; verum