len (<%x,(1. L)%> `^ n) = n + 1 by Th36;
hence <%x,(1. L)%> `^ n is non-zero by Th14; :: thesis: verum