let n be set ; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds
( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) )
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds
( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) )
let p be Series of n,L; :: thesis: ( p is Monomial of n,L iff ( Support p = {} or ex b being bag of n st Support p = {b} ) )

A1: now :: thesis: ( ex b being bag of n st Support p = {b} implies p is Monomial of n,L )

assume ex b being bag of n st Support p = {b} ; :: thesis: p is Monomial of n,L
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: ( b9 <> b implies p . b9 = 0. L )
assume A3: b9 <> b ; :: thesis: p . b9 = 0. L
assume A4: p . b9 <> 0. L ; :: thesis: contradiction
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: verum

end;

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

end;

A5: now :: thesis: ( not p is Monomial of n,L or Support p = {} or ex b being bag of n st Support p = {b} )

assume p is Monomial of n,L ; :: thesis: ( Support p = {} or ex b being bag of n st Support p = {b} )
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: ( ( p . b <> 0. L & ex b being bag of n st Support p = {b} ) or ( p . b = 0. L & Support p = {} ) )

per cases ( p . b <> 0. L or p . b = 0. L ) ;

case A7: p . b <> 0. L ; :: thesis: ex b being bag of n st Support p = {b}

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

proof

let u be object ; :: thesis: ( u in {b} implies u in Support p )
assume A9: u in {b} ; :: thesis: u in Support p
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: verum

end;

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

proof

let u be object ; :: thesis: ( u in Support p implies u in {b} )
assume A10: u in Support p ; :: thesis: u in {b}
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: verum

end;

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

end;

case A11: p . b = 0. L ; :: thesis: Support p = {}

thus Support p = {} :: thesis: verum

proof

assume Support p <> {} ; :: thesis: contradiction
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: verum

end;

end;

end;

end;

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

end;

now :: thesis: ( Support p = {} implies p is Monomial of n,L )

set b = the bag of n;
assume A12: Support p = {} ; :: thesis: p is Monomial of n,L
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: ( b9 <> the bag of n implies p . b9 = 0. L )
assume b9 <> the bag of n ; :: thesis: p . b9 = 0. L
reconsider c = b9 as Element of Bags n by PRE_POLY:def 12;
assume p . b9 <> 0. L ; :: thesis: contradiction
then c in Support p by POLYNOM1:def 4;
hence contradiction by A12; :: thesis: verum

end;

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

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: verum