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 = {}

A2: now

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

end;

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