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