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