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: now :: thesis: ( f . x = y implies x = (f ") . y )

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

end;

rng f = A by FUNCT_2:def 3;
hence ( f . x = y iff (f ") . y = x ) by A1, FUNCT_1:35; :: thesis: verum