Sum F = addint "**" F by Th50;
hence Sum F is integer ; :: thesis: verum