A2: dom (r (#) f) = dom f by Def5;
thus dom (r (#) f) c= X by A2; :: according to RELAT_1:def 18 :: thesis: verum