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 set st x in dom f holds
not x in dom g

proof

let x be set ; :: 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 FUNCT_1:def 2;

now

assume x in dom g ; :: thesis: contradiction
then A5: [x,(g . x)] in g by FUNCT_1:def 2;
then f . x = g . x by A1, A2, A4, FUNCT_1:def 1;
hence contradiction by A3, A4, A5, Lm3; :: thesis: verum

end;

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

end;

hence dom f misses dom g by Lm3; :: thesis: verum