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