Product F = multnat "**" F by Th3;
hence Product F is natural ; :: thesis: verum