A: dom (f - r) = dom f by Th3;
dom f c= X by RELAT_1:def 18;
hence dom (f - r) c= X by A; :: according to RELAT_1:def 18 :: thesis: verum