let f be Function; :: thesis: ( f is one-to-one iff for y being set st y in rng f holds
f just_once_values y )
thus ( f is one-to-one implies for y being set st y in rng f holds
f just_once_values y ) :: thesis: ( ( for y being set 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 set st y in rng f holds
f just_once_values y
let y be set ; :: 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 set such that
A2: ( x in dom f & f . x = y ) by FUNCT_1:def 5;
for z being set st z in dom f & z <> x holds
f . z <> y by A1, A2, FUNCT_1:def 8;
hence f just_once_values y by A2, Th9; :: thesis: verum

end;

assume A3: for y being set st y in rng f holds
f just_once_values y ; :: thesis: f is one-to-one
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 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 5;
then f just_once_values f . x by A3;
then consider x1 being set such that
A6: {x1} = f " {(f . x)} by Th8;
A7: f . x in {(f . x)} by TARSKI:def 1;
then A8: y in f " {(f . x)} by A5, FUNCT_1:def 13;
x in f " {(f . x)} by A4, A7, FUNCT_1:def 13;
then x = x1 by A6, TARSKI:def 1;
hence x = y by A6, A8, TARSKI:def 1; :: thesis: verum