ex n being Nat st dom p = n by Th7;
hence dom p is natural ; :: thesis: verum