let f be Function; :: thesis: for y being set holds
( f just_once_values y iff ex x being set st {x} = f " {y} )
let y be set ; :: thesis: ( f just_once_values y iff ex x being set st {x} = f " {y} )
thus ( f just_once_values y implies ex x being set st {x} = f " {y} ) :: thesis: ( ex x being set st {x} = f " {y} implies f just_once_values y )

proof

assume A1: f just_once_values y ; :: thesis: ex x being set st {x} = f " {y}
then y in rng f by Th7;
then consider x being set such that
A2: x in dom f and
A3: f . x = y by FUNCT_1:def 5;
take x ; :: thesis: {x} = f " {y}
ex B being finite set st
( B = f " {y} & card B = 1 ) by A1, Def2;
then consider z being set such that
A4: f " {y} = {z} by CARD_2:60;
f . x in {y} by A3, TARSKI:def 1;
then x in {z} by A2, A4, FUNCT_1:def 13;
hence {x} = f " {y} by A4, TARSKI:def 1; :: thesis: verum

end;

given x being set such that A5: {x} = f " {y} ; :: thesis: f just_once_values y
reconsider B = f " {y} as finite set by A5;
take B ; :: according to FINSEQ_4:def 2 :: thesis: ( B = f " {y} & card B = 1 )
thus ( B = f " {y} & card B = 1 ) by A5, CARD_1:50; :: thesis: verum