let f be Function; :: thesis: for x being set st not x in rng f holds
f " {x} = {}
let x be set ; :: thesis: ( not x in rng f implies f " {x} = {} )
assume A1: not x in rng f ; :: thesis: f " {x} = {}
rng f misses {x}

proof

set y = the Element of (rng f) /\ {x};
assume (rng f) /\ {x} <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then ( the Element of (rng f) /\ {x} in rng f & the Element of (rng f) /\ {x} in {x} ) by XBOOLE_0:def 4;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

hence f " {x} = {} by RELAT_1:138; :: thesis: verum