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