A3: dom (f ^2) = dom f by Th11;
thus dom (f ^2) c= X by A3; :: according to RELAT_1:def 18 :: thesis: verum