( z0 <> 0. L or z0 = 0. L ) ;
then ( len <%z1,z0%> = 2 or len <%z1,z0%> = 1 ) by POLYNOM5:40, POLYNOM5:41;
hence <%z1,z0%> is non-zero by UPROOTS:17; :: thesis: verum