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 dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: 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 & y in dom f ) and
A5: f . x = f . y ; :: thesis: x = y
( f . x in rng f & f . y in rng f ) by A4, FUNCT_1:def 5;
then ( f just_once_values f . x & f just_once_values f . y ) by A3;
then consider x1 being set such that
A6: {x1} = f " {(f . x)} by Th8;
( f . x in {(f . x)} & f . y in {(f . y)} ) by TARSKI:def 1;
then ( x in f " {(f . x)} & y in f " {(f . x)} ) by A4, A5, FUNCT_1:def 13;
then ( x = x1 & y = x1 ) by A6, TARSKI:def 1;
hence x = y ; :: thesis: verum