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

now :: thesis: not rng F meets {x}

assume rng F meets {x} ; :: thesis: contradiction
then ex y being object st
( y in rng F & y in {x} ) by XBOOLE_0:3;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

hence Coim (F,x) = {} by RELAT_1:138; :: thesis: verum