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