let f be Function; :: thesis: for y being set st f just_once_values y holds
y in rng f
let y be set ; :: thesis: ( f just_once_values y implies y in rng f )
assume f just_once_values y ; :: thesis: y in rng f
then ex B being finite set st
( B = f " {y} & card B = 1 ) by Def2;
then rng f meets {y} by CARD_1:47, RELAT_1:173;
then consider x being set such that
A1: x in (rng f) /\ {y} by XBOOLE_0:4;
x in {y} by A1, XBOOLE_0:def 4;
then y = x by TARSKI:def 1;
hence y in rng f by A1, XBOOLE_0:def 4; :: thesis: verum