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

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