let f, g be Function; :: thesis: ( f c= g implies disjoin f c= disjoin g )
assume f c= g ; :: thesis: disjoin f c= disjoin g
then A1: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) by GRFUNC_1:8;
A2: ( dom (disjoin f) = dom f & dom (disjoin g) = dom g ) by Def3;

now

let x be set ; :: thesis: ( x in dom (disjoin f) implies (disjoin f) . x = (disjoin g) . x )
assume x in dom (disjoin f) ; :: thesis: (disjoin f) . x = (disjoin g) . x
then ( (disjoin f) . x = [:(f . x),{x}:] & (disjoin g) . x = [:(g . x),{x}:] & f . x = g . x ) by A1, A2, Def3;
hence (disjoin f) . x = (disjoin g) . x ; :: thesis: verum

end;

hence disjoin f c= disjoin g by A1, A2, GRFUNC_1:8; :: thesis: verum