let A be non empty set ; :: thesis: for f, g being Permutation of A
for R being Relation of [:A,A:] st f is_automorphism_of R & g is_automorphism_of R holds
g * f is_automorphism_of R
let f, g be Permutation of A; :: thesis: for R being Relation of [:A,A:] st f is_automorphism_of R & g is_automorphism_of R holds
g * f is_automorphism_of R
let R be Relation of [:A,A:]; :: thesis: ( f is_automorphism_of R & g is_automorphism_of R implies g * f is_automorphism_of R )
assume A1: ( ( for x, y, z, t being Element of A holds
( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) ) & ( 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 3 :: thesis: g * f is_automorphism_of R
let x be Element of A; :: according to TRANSGEO:def 3 :: thesis: for y, z, t being Element of A holds
( [[x,y],[z,t]] in R iff [[((g * f) . x),((g * f) . y)],[((g * f) . z),((g * f) . t)]] in R )
let y, z, t be Element of A; :: thesis: ( [[x,y],[z,t]] in R iff [[((g * f) . x),((g * f) . y)],[((g * f) . z),((g * f) . t)]] in R )
A2: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y & g . (f . z) = (g * f) . z & g . (f . t) = (g * f) . t ) by FUNCT_2:21;
( ( [[x,y],[z,t]] in R implies [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) & ( [[(f . x),(f . y)],[(f . z),(f . t)]] in R implies [[x,y],[z,t]] in R ) & ( [[(f . x),(f . y)],[(f . z),(f . t)]] in R implies [[(g . (f . x)),(g . (f . y))],[(g . (f . z)),(g . (f . t))]] in R ) & ( [[(g . (f . x)),(g . (f . y))],[(g . (f . z)),(g . (f . t))]] in R implies [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) ) by A1;
hence ( [[x,y],[z,t]] in R iff [[((g * f) . x),((g * f) . y)],[((g * f) . z),((g * f) . t)]] in R ) by A2; :: thesis: verum