let f be Function; :: thesis: for y being object st f just_once_values y holds
y in rng f
let y be object ; :: thesis: ( f just_once_values y implies y in rng f )
assume f just_once_values y ; :: thesis: y in rng f
then card (Coim (f,y)) = 1 ;
then rng f meets {y} by CARD_1:27, RELAT_1:138;
then consider x being object 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