let X, Y be set ; :: thesis: for f being Function st f is one-to-one holds
<:f,X,Y:> is one-to-one
let f be Function; :: thesis: ( f is one-to-one implies <:f,X,Y:> is one-to-one )
assume f is one-to-one ; :: thesis: <:f,X,Y:> is one-to-one
then Y |` f is one-to-one by FUNCT_1:58;
hence <:f,X,Y:> is one-to-one by FUNCT_1:52; :: thesis: verum