dom (g +* f) = (dom g) \/ (dom f) by Def1;
hence not g +* f is empty ; :: thesis: verum