let g, f 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 set st [x1,y] in g & [x2,y] in g holds
x1 = x2 by Th25;
hence g is one-to-one by Th25; :: thesis: verum