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