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