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 Th2;
( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2;
hence ( [[x,y],[z,t]] in R iff [[((f ") . x),((f ") . y)],[((f ") . z),((f ") . t)]] in R ) by A1, A2; :: thesis: verum