A2: dom (f ") = dom f by Def7;
dom f = X by PARTFUN1:def 2;
hence f " is total by A2, PARTFUN1:def 2; :: thesis: verum