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