let F be Function; :: thesis: for x being set st not x in rng F holds
Coim F,x = {}
let x be set ; :: thesis: ( not x in rng F implies Coim F,x = {} )
assume A1: not x in rng F ; :: thesis: Coim F,x = {}

now

assume rng F meets {x} ; :: thesis: contradiction
then consider y being set such that
A2: ( y in rng F & y in {x} ) by XBOOLE_0:3;
thus contradiction by A1, A2, TARSKI:def 1; :: thesis: verum

end;

hence Coim F,x = {} by RELAT_1:173; :: thesis: verum