let f be Function; :: thesis: ( f is oneone implies f is one-to-one )
set D = dom f;
assume f is oneone ; :: thesis: f is one-to-one
then reconsider g = f ~ as Function ;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then ( [x1,(f . x1)] in f & [x2,(f . x1)] in f ) by FUNCT_1:def 2;
then ( [(f . x1),x1] in g & [(f . x1),x2] in g ) by RELAT_1:def 7;
hence x1 = x2 by FUNCT_1:def 1; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 4; :: thesis: verum