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