dom (f * g) c= dom g by RELAT_1:25;
hence f * g is finite by Th10; :: thesis: verum