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

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

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

hence
p is Monomial of n,L
by Def3; :: thesis: verum
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;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

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;

end;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 = {} ) )end;

hence
( Support p = {} or ex b being bag of n st Support p = {b} )
; :: thesis: verumper cases
( p . b <> 0. L or p . b = 0. L )
;

end;

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

u in {b}

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

end;u in Support p

proof

for u being object st u in Support p holds
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;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

u in {b}

proof

then
Support p = {b}
by A8, TARSKI:2;
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;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

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

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

thus
Support p = {}
:: thesis: verum

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

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

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

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

hence
p is Monomial of n,L
by Def3; :: thesis: verum
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;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