set a = the Element of NonZero L;
reconsider a = the Element of NonZero L as Element of L ;
take p = <%a%>; :: thesis: p is non-zero
A1: ( not a in {(0. L)} & (0_. L) . 0 = 0. L ) by FUNCOP_1:7, XBOOLE_0:def 5;
p . 0 = a by POLYNOM5:32;
then p <> 0_. L by A1, TARSKI:def 1;
hence p is non-zero ; :: thesis: verum