let f, g be Function; :: thesis: ( g c= f & f is one-to-one implies g is one-to-one )
assume ( g c= f & f is one-to-one ) ; :: thesis: g is one-to-one
then for x1, x2, y being object st [x1,y] in g & [x2,y] in g holds
x1 = x2 by Th9;
hence g is one-to-one by Th9; :: thesis: verum