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