A1: dom (r + f) = dom f by Def2;
thus dom (r + f) c= X by A1; :: according to RELAT_1:def 18 :: thesis: verum