A: dom |.f.| = dom f by Def11;
dom f = X by PARTFUN1:def 2;
hence |.f.| is total by A, PARTFUN1:def 2; :: thesis: verum