Product F = multreal "**" F by Th1;
hence Product F is real ; :: thesis: verum