let f be Function; :: thesis: ( f is one-to-one implies for x, y being object holds
( [y,x] in f " iff [x,y] in f ) )
assume A1: f is one-to-one ; :: thesis: for x, y being object holds
( [y,x] in f " iff [x,y] in f )
let x, y be object ; :: thesis: ( [y,x] in f " iff [x,y] in f )
dom (f ") = rng f by A1, FUNCT_1:33;
then ( y in dom (f ") & x = (f ") . y iff ( x in dom f & y = f . x ) ) by A1, FUNCT_1:32;
hence ( [y,x] in f " iff [x,y] in f ) by FUNCT_1:1; :: thesis: verum