let f be Function; :: thesis: ( f is one-to-one implies f " is one-to-one )
assume A1: f is one-to-one ; :: thesis: f " is one-to-one
let y1 be set ; :: according to FUNCT_1:def 8 :: thesis: for x2 being set st y1 in dom (f " ) & x2 in dom (f " ) & (f " ) . y1 = (f " ) . x2 holds
y1 = x2
let y2 be set ; :: thesis: ( y1 in dom (f " ) & y2 in dom (f " ) & (f " ) . y1 = (f " ) . y2 implies y1 = y2 )
assume ( y1 in dom (f " ) & y2 in dom (f " ) ) ; :: thesis: ( not (f " ) . y1 = (f " ) . y2 or y1 = y2 )
then ( y1 in rng f & y2 in rng f ) by A1, Th54;
then ( y1 = f . ((f " ) . y1) & y2 = f . ((f " ) . y2) ) by A1, Th57;
hence ( not (f " ) . y1 = (f " ) . y2 or y1 = y2 ) ; :: thesis: verum