A1: dom (- f) = dom f by Def5;
dom f = X by PARTFUN1:def 2;
hence - f is total by A1, PARTFUN1:def 2; :: thesis: verum