dom (f | X) c= X by RELAT_1:58;
hence dom (f | X) is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum