let n be set ; :: thesis:
let L be non empty ZeroStr ; :: thesis:
let p be Series of n,L; :: thesis:

A1: now :: thesis:

assume ex b being bag of n st Support p = {b} ; :: thesis:
then consider b being bag of n such that
A2: Support p = {b} ;
for b9 being bag of n st b9 <> b holds
p . b9 = 0. L

proof

let b9 be bag of n; :: thesis:
assume A3: b9 <> b ; :: thesis:
assume A4: p . b9 <> 0. L ; :: thesis:
reconsider b9 = b9 as Element of Bags n by PRE_POLY:def 12;
b9 in Support p by A4, POLYNOM1:def 4;
hence contradiction by A2, A3, TARSKI:def 1; :: thesis:

end;

hence p is Monomial of n,L by Def3; :: thesis:

end;

A5: now :: thesis:

assume p is Monomial of n,L ; :: thesis:
then consider b being bag of n such that
A6: for b9 being bag of n st b9 <> b holds
p . b9 = 0. L by Def3;

now :: thesis:

per cases ;

case A7: p . b <> 0. L ; :: thesis:

A8: for u being object st u in {b} holds
u in Support p

proof

let u be object ; :: thesis:
assume A9: u in {b} ; :: thesis:
then u = b by TARSKI:def 1;
then reconsider u9 = u as Element of Bags n by PRE_POLY:def 12;
p . u9 <> 0. L by A7, A9, TARSKI:def 1;
hence u in Support p by POLYNOM1:def 4; :: thesis:

end;

for u being object st u in Support p holds
u in {b}

proof

let u be object ; :: thesis:
assume A10: u in Support p ; :: thesis:
then reconsider u9 = u as bag of n ;
p . u <> 0. L by A10, POLYNOM1:def 4;
then u9 = b by A6;
hence u in {b} by TARSKI:def 1; :: thesis:

end;

then Support p = {b} by A8, TARSKI:2;
hence ex b being bag of n st Support p = {b} ; :: thesis:

end;

case A11: p . b = 0. L ; :: thesis:

thus Support p = {} :: thesis:

proof

assume Support p <> {} ; :: thesis:
then reconsider sp = Support p as non empty Subset of (Bags n) ;
set c = the Element of sp;
p . the Element of sp <> 0. L by POLYNOM1:def 4;
hence contradiction by A6, A11; :: thesis:

end;

end;

end;

end;

hence ( Support p = {} or ex b being bag of n st Support p = {b} ) ; :: thesis:

end;

now :: thesis:

set b = the bag of n;
assume A12: Support p = {} ; :: thesis:
for b9 being bag of n st b9 <> the bag of n holds
p . b9 = 0. L

proof

let b9 be bag of n; :: thesis:
assume b9 <> the bag of n ; :: thesis:
reconsider c = b9 as Element of Bags n by PRE_POLY:def 12;
assume p . b9 <> 0. L ; :: thesis:
then c in Support p by POLYNOM1:def 4;
hence contradiction by A12; :: thesis:

end;

hence p is Monomial of n,L by Def3; :: thesis:

end;

hence ( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) ) by A1, A5; :: thesis: