let f, g be one-to-one Function; :: thesis: ( f " = g " implies f = g )
( (f ") " = f & (g ") " = g ) by FUNCT_1:43;
hence ( f " = g " implies f = g ) ; :: thesis: verum