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_ (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 :: thesis: for u being object st u in Support p holds
u in {(EmptyBag n)}

let u be object ; :: thesis: ( u in Support p implies u in {(EmptyBag n)} )
assume A3: u in Support p ; :: thesis: u in {(EmptyBag n)}
then u is Element of Bags n ;
then A4: u is bag of n ;

now :: thesis: not u <> EmptyBag n

assume u <> EmptyBag n ; :: thesis: contradiction
then p . u = (0_ (n,R)) . u by FUNCT_7:32
.= 0. R by A4, POLYNOM1:22 ;
hence contradiction by A3, POLYNOM1:def 4; :: 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 8;
then dom (0_ (n,R)) = Bags n ;
then A5: p . (EmptyBag n) = a by FUNCT_7:31;

now :: thesis: for u being object st u in {(EmptyBag n)} holds
u in Support p

let u be object ; :: 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 4; :: thesis: verum

end;

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