Sum F = addnat "**" F by Th63;
hence Sum F is natural ; :: thesis: verum