let A be non empty set ; :: thesis: for x, y being Element of A
for f being Permutation of A holds
( f . x = y iff (f " ) . y = x )
let x, y be Element of A; :: thesis: for f being Permutation of A holds
( f . x = y iff (f " ) . y = x )
let f be Permutation of A; :: thesis: ( f . x = y iff (f " ) . y = x )
A1: ( f is one-to-one & rng f = A & f is Function of A,A ) by FUNCT_2:def 3;

now

assume f . x = y ; :: thesis: x = (f " ) . y
then ( (f " ) . (f . x) = (f " ) . y & x in A ) ;
then ( (f " ) . (f . x) = (f " ) . y & x in dom f ) by FUNCT_2:def 1;
hence x = (f " ) . y by FUNCT_1:56; :: thesis: verum

end;

hence ( f . x = y iff (f " ) . y = x ) by A1, FUNCT_1:57; :: thesis: verum