let f, g, h be Function; :: thesis: ( f c= h & g c= h & f misses g implies dom f misses dom g )
assume that
A1: f c= h and
A2: g c= h and
A3: f misses g ; :: thesis: dom f misses dom g
for x being object st x in dom f holds
not x in dom g

proof

let x be object ; :: thesis: ( x in dom f implies not x in dom g )
assume x in dom f ; :: thesis: not x in dom g
then A4: [x,(f . x)] in f by Def2;

now :: thesis: not x in dom g

assume x in dom g ; :: thesis: contradiction
then A5: [x,(g . x)] in g by Def2;
then f . x = g . x by A1, A2, A4, Def1;
hence contradiction by A3, A4, A5, XBOOLE_0:3; :: thesis: verum

end;

hence not x in dom g ; :: thesis: verum

end;

hence dom f misses dom g by XBOOLE_0:3; :: thesis: verum