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