let f, g be Function; :: thesis: ( dom f c= dom (f +* g) & dom g c= dom (f +* g) )
dom (f +* g) = (dom f) \/ (dom g) by Def1;
hence ( dom f c= dom (f +* g) & dom g c= dom (f +* g) ) by XBOOLE_1:7; :: thesis: verum