set a = the Element of NonZero R;
A1: not the Element of NonZero R in {(0. R)} by XBOOLE_0:def 5;
reconsider a = the Element of NonZero R as Element of R ;
set p = (0_ (X,R)) +* ((EmptyBag X),a);
reconsider p = (0_ (X,R)) +* ((EmptyBag X),a) as Function of (Bags X), the carrier of R ;
reconsider p = p as Function of (Bags X),R ;
reconsider p = p as Series of X,R ;
take p ; :: thesis: p is non-zero
0_ (X,R) = (Bags X) --> (0. R) by POLYNOM1:def 8;
then dom (0_ (X,R)) = Bags X ;
then A2: p . (EmptyBag X) = a by FUNCT_7:31;
a <> 0. R by A1, TARSKI:def 1;
then p <> 0_ (X,R) by A2, POLYNOM1:22;
hence p is non-zero ; :: thesis: verum