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 that
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 ) 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 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 )
A3: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15;
A4: ( g . (f . z) = (g * f) . z & g . (f . t) = (g * f) . t ) by FUNCT_2:15;
( [[x,y],[z,t]] in R iff [[(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, A3, A4; :: thesis: verum