dom (f * g) c= dom g by RELAT_1:44;
then dom (f * g) is finite ;
hence f * g is finite by Th29; :: thesis: verum