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