consider a being Element of NonZero R;
A1: not a in {(0. R)} by XBOOLE_0:def 5;
reconsider a = a 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 24;
then dom (0_ X,R) = Bags X by FUNCOP_1:19;
then A2: p . (EmptyBag X) = a by FUNCT_7:33;
a <> 0. R by A1, TARSKI:def 1;
then p <> 0_ X,R by A2, POLYNOM1:81;
hence p is non-zero by Def2; :: thesis: verum