A: dom (r (#) f) = dom f by Def5;
dom f = X by PARTFUN1:def 2;
hence r (#) f is total by A, PARTFUN1:def 2; :: thesis: verum