dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def4;
then A2: dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17;
thus dom (f1 (#) f2) c= X by A2, XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum