let f be Function; :: thesis: for y1, y2 being object st f is one-to-one & y1 in rng f & f " {y1} = f " {y2} holds
y1 = y2
let y1, y2 be object ; :: thesis: ( f is one-to-one & y1 in rng f & f " {y1} = f " {y2} implies y1 = y2 )
assume that
A1: ( f is one-to-one & y1 in rng f ) and
A2: f " {y1} = f " {y2} ; :: thesis: y1 = y2
consider x1 being object such that
A3: f " {y1} = {x1} by A1, FUNCT_1:74;
f . x1 = y1 by A3, Th3;
hence y1 = y2 by A2, A3, Th3; :: thesis: verum