dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
hence f +* g is finite by Th10; :: thesis: verum