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