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 )

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

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 )

rng f = A
by FUNCT_2:def 3;
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;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

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