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