A1: dom (r + f) = dom f by Def2;
dom f = X by PARTFUN1:def 2;
hence r + f is total by A1, PARTFUN1:def 2; :: thesis: verum