len <%x,(1. L)%> = 2 by POLYNOM5:40;
hence <%x,(1. L)%> is non-zero by Th19; :: thesis: verum