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