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