A2: dom (f ") = dom f by Def7;
thus dom (f ") c= X by A2; :: according to RELAT_1:def 18 :: thesis: verum