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 that
A2: y1 in dom (f " ) and
A3: y2 in dom (f " ) ; :: thesis: ( not (f " ) . y1 = (f " ) . y2 or y1 = y2 )
y1 in rng f by A1, A2, Th54;
then A4: y1 = f . ((f " ) . y1) by A1, Th57;
y2 in rng f by A1, A3, Th54;
hence ( not (f " ) . y1 = (f " ) . y2 or y1 = y2 ) by A1, A4, Th57; :: thesis: verum