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