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 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 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 st Support p = {b} ) )

A1: now

assume A2: Support p = {} ; :: thesis: p is Monomial of n,L
consider b being bag of ;
for b' being bag of st b' <> b holds
p . b' = 0. L

proof

let b' be bag of ; :: thesis: ( b' <> b implies p . b' = 0. L )
assume b' <> b ; :: thesis: p . b' = 0. L
assume A3: p . b' <> 0. L ; :: thesis: contradiction
reconsider c = b' as Element of Bags n by POLYNOM1:def 14;
c in Support p by A3, POLYNOM1:def 9;
hence contradiction by A2; :: thesis: verum

end;

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

end;

A4: now

assume ex b being bag of st Support p = {b} ; :: thesis: p is Monomial of n,L
then consider b being bag of such that
A5: Support p = {b} ;
for b' being bag of st b' <> b holds
p . b' = 0. L

proof

let b' be bag of ; :: thesis: ( b' <> b implies p . b' = 0. L )
assume A6: b' <> b ; :: thesis: p . b' = 0. L
assume A7: p . b' <> 0. L ; :: thesis: contradiction
reconsider b' = b' as Element of Bags n by POLYNOM1:def 14;
b' in Support p by A7, POLYNOM1:def 9;
hence contradiction by A5, A6, TARSKI:def 1; :: thesis: verum

end;

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

end;

now

assume p is Monomial of n,L ; :: thesis: ( Support p = {} or ex b being bag of st Support p = {b} )
then consider b being bag of such that
A8: for b' being bag of st b' <> b holds
p . b' = 0. L by Def4;

now

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

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

A10: for u being set st u in Support p holds
u in {b}

proof

let u be set ; :: thesis: ( u in Support p implies u in {b} )
assume A11: u in Support p ; :: thesis: u in {b}
then A12: p . u <> 0. L by POLYNOM1:def 9;
reconsider u' = u as bag of by A11, POLYNOM1:def 14;
u' = b by A8, A12;
hence u in {b} by TARSKI:def 1; :: thesis: verum

end;

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

proof

let u be set ; :: thesis: ( u in {b} implies u in Support p )
assume A13: u in {b} ; :: thesis: u in Support p
then u = b by TARSKI:def 1;
then reconsider u' = u as Element of Bags n by POLYNOM1:def 14;
p . u' <> 0. L by A9, A13, TARSKI:def 1;
hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

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

end;

case A14: 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) ;
consider c being Element of sp;
c in Support p ;
then p . c <> 0. L by POLYNOM1:def 9;
hence contradiction by A8, A14; :: thesis: verum

end;

end;

end;

end;

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

end;

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