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