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 object ; :: according to FUNCT_1:def 4 :: thesis: for x2 being object st y1 in dom (f ") & x2 in dom (f ") & (f ") . y1 = (f ") . x2 holds
y1 = x2
let y2 be object ; :: 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, Th31;
then A4: y1 = f . ((f ") . y1) by A1, Th34;
y2 in rng f by A1, A3, Th31;
hence ( not (f ") . y1 = (f ") . y2 or y1 = y2 ) by A1, A4, Th34; :: thesis: verum