let A be non empty set ; :: thesis: 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; :: thesis: 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:]; :: thesis: ( 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 ) ; :: according to TRANSGEO:def 2,TRANSGEO:def 3 :: thesis: f \ g is_FormalIz_of R
let x be Element of A; :: according to TRANSGEO:def 2 :: thesis: for y being Element of A holds [[x,y],[((f \ g) . x),((f \ g) . y)]] in R
let y be Element of A; :: thesis: [[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; :: thesis: verum