let f be Function; :: thesis: ( f is one-to-one iff for y being object st y in rng f holds
f just_once_values y )
thus ( f is one-to-one implies for y being object st y in rng f holds
f just_once_values y ) :: thesis: ( ( for y being object st y in rng f holds
f just_once_values y ) implies f is one-to-one )

proof

assume A1: f is one-to-one ; :: thesis: for y being object st y in rng f holds
f just_once_values y
let y be object ; :: thesis: ( y in rng f implies f just_once_values y )
assume y in rng f ; :: thesis: f just_once_values y
then consider x being object such that
A2: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
for z being object st z in dom f & z <> x holds
f . z <> y by A1, A2;
hence f just_once_values y by A2, Th7; :: thesis: verum

end;

assume A3: for y being object st y in rng f holds
f just_once_values y ; :: thesis: f is one-to-one
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A4: x in dom f and
A5: ( y in dom f & f . x = f . y ) ; :: thesis: x = y
f . x in rng f by A4, FUNCT_1:def 3;
then f just_once_values f . x by A3;
then consider x1 being object such that
A6: {x1} = f " {(f . x)} by Th6;
A7: f . x in {(f . x)} by TARSKI:def 1;
then A8: y in f " {(f . x)} by A5, FUNCT_1:def 7;
x in f " {(f . x)} by A4, A7, FUNCT_1:def 7;
then x = x1 by A6, TARSKI:def 1;
hence x = y by A6, A8, TARSKI:def 1; :: thesis: verum