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