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