consider a being Element of the carrier of R \ {(0. R)};
A1: not the carrier of R \ {(0. R)} is empty by REALSET1:4;
then A2: ( a in the carrier of R & not a in {(0. R)} ) by XBOOLE_0:def 5;
reconsider a = a as Element of R by A1, XBOOLE_0:def 5;
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 A3: p . (EmptyBag X) = a by FUNCT_7:33;
a <> 0. R by A2, TARSKI:def 1;
then p <> 0_ X,R by A3, POLYNOM1:81;
hence p is non-zero by Def2; :: thesis: verum