let R be Function; :: thesis: ( R ~ is Function implies R is one-to-one )
assume A0: R ~ is Function ; :: thesis: R is one-to-one
assume not R is one-to-one ; :: thesis: contradiction
then consider x1, x2 being object such that
A1: ( x1 in dom R & x2 in dom R & R . x1 = R . x2 & x1 <> x2 ) by FUNCT_1:def 4;
[x1,(R . x1)] in R by A1, FUNCT_1:def 2;
then A2: [(R . x1),x1] in R ~ by RELAT_1:def 7;
[x2,(R . x2)] in R by A1, FUNCT_1:def 2;
then [(R . x2),x2] in R ~ by RELAT_1:def 7;
hence contradiction by A1, A2, A0, FUNCT_1:def 1; :: thesis: verum