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_ 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 ;

A2: now

let u be set ; :: thesis: ( u in Support p implies u in {(EmptyBag n)} )
assume A3: u in Support p ; :: thesis: u in {(EmptyBag n)}
then A4: 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 A4, POLYNOM1:81 ;
hence contradiction by A3, POLYNOM1:def 9; :: thesis: verum

end;

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

end;

0_ n,R = (Bags n) --> (0. R) by POLYNOM1:def 24;
then dom (0_ n,R) = Bags n by FUNCOP_1:19;
then A5: p . (EmptyBag n) = a by FUNCT_7:33;

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 A6: u = EmptyBag n by TARSKI:def 1;
a <> 0. R by A1, TARSKI:def 1;
hence u in Support p by A5, A6, POLYNOM1:def 9; :: thesis: verum

end;

then Support p = {(EmptyBag n)} by A2, 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 A1, TARSKI:def 1;
then p <> 0_ n,R by A5, POLYNOM1:81;
hence p is non-zero by Def2; :: thesis: verum