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