dom (f | X) c= X by RELAT_1:87;
hence dom (f | X) is with_common_domain ; :: according to UNIALG_1:def 1 :: thesis: verum