A3: dom (f ^2) = dom f by Th11;
dom f = X by PARTFUN1:def 2;
hence f ^2 is total by A3, PARTFUN1:def 2; :: thesis: verum