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