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