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