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