Sum F = addrat "**" F by Th62;
hence Sum F is rational ; :: thesis: verum