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

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