Sum F = addreal "**" F by Th60;
hence Sum F is real ; :: thesis: verum