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 ;

then dom (0_ (n,R)) = Bags n ;

then A5: p . (EmptyBag n) = a by FUNCT_7:31;

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

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)}

0_ (n,R) = (Bags n) --> (0. R)
by POLYNOM1:def 8;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 ;

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

hence
u in {(EmptyBag n)}
by TARSKI:def 1; :: thesis: verumassume
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;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

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

then
Support p = {(EmptyBag n)}
by A2, TARSKI:2;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;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

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