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_ n,R) +* (EmptyBag n),a;
reconsider p = (0_ n,R) +* (EmptyBag n),a as Function of Bags n,the carrier of R ;
reconsider p = p as Function of Bags n,R ;
reconsider p = p as Series of n,R ;
0_ n,R = (Bags n) --> (0. R) by POLYNOM1:def 24;
then dom (0_ n,R) = Bags n by FUNCOP_1:19;
then A3: p . (EmptyBag n) = a by FUNCT_7:33;

A4: now

let u be set ; :: thesis: ( u in {(EmptyBag n)} implies u in Support p )
assume u in {(EmptyBag n)} ; :: thesis: u in Support p
then A5: u = EmptyBag n by TARSKI:def 1;
a <> 0. R by A2, TARSKI:def 1;
hence u in Support p by A3, A5, POLYNOM1:def 9; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in Support p implies u in {(EmptyBag n)} )
assume A6: u in Support p ; :: thesis: u in {(EmptyBag n)}
then A7: u is Element of Bags n ;

now

assume u <> EmptyBag n ; :: thesis: contradiction
then p . u = (0_ n,R) . u by FUNCT_7:34
.= 0. R by A7, POLYNOM1:81 ;
hence contradiction by A6, POLYNOM1:def 9; :: thesis: verum

end;

hence u in {(EmptyBag n)} by TARSKI:def 1; :: thesis: verum

end;

then Support p = {(EmptyBag n)} by A4, TARSKI:2;
then reconsider p = p as Polynomial of n,R by POLYNOM1:def 10;
take p ; :: thesis: p is non-zero
a <> 0. R by A2, TARSKI:def 1;
then p <> 0_ n,R by A3, POLYNOM1:81;
hence p is non-zero by Def2; :: thesis: verum