dom (g * f) c= dom f by RELAT_1:44;
hence dom (g * f) is with_common_domain ; :: according to UNIALG_1:def 1 :: thesis: verum