let f, g be Function; :: thesis: ( f c= g implies disjoin f c= disjoin g )
assume A1: f c= g ; :: thesis: disjoin f c= disjoin g
then A2: dom f c= dom g by GRFUNC_1:2;
A3: dom (disjoin f) = dom f by Def3;
A4: dom (disjoin g) = dom g by Def3;

now :: thesis: for x being object st x in dom (disjoin f) holds
(disjoin f) . x = (disjoin g) . x

let x be object ; :: thesis: ( x in dom (disjoin f) implies (disjoin f) . x = (disjoin g) . x )
assume A5: x in dom (disjoin f) ; :: thesis: (disjoin f) . x = (disjoin g) . x
then A6: (disjoin f) . x = [:(f . x),{x}:] by A3, Def3;
f . x = g . x by A1, A3, A5, GRFUNC_1:2;
hence (disjoin f) . x = (disjoin g) . x by A2, A3, A5, A6, Def3; :: thesis: verum

end;

hence disjoin f c= disjoin g by A2, A3, A4, GRFUNC_1:2; :: thesis: verum