let s be Series of X,L; :: thesis: ( s is monomial-like implies s is finite-Support )

assume s is monomial-like ; :: thesis: s is finite-Support

then consider b being bag of X such that

A1: for b9 being bag of X st b9 <> b holds

s . b9 = 0. L ;

assume s is monomial-like ; :: thesis: s is finite-Support

then consider b being bag of X such that

A1: for b9 being bag of X st b9 <> b holds

s . b9 = 0. L ;

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

end;

suppose A2:
s . b = 0. L
; :: thesis: s is finite-Support

end;

now :: thesis: not Support s <> {}

hence
s is finite-Support
by POLYNOM1:def 5; :: thesis: verumassume
Support s <> {}
; :: thesis: contradiction

then reconsider sp = Support s as non empty Subset of (Bags X) ;

set c = the Element of sp;

s . the Element of sp <> 0. L by POLYNOM1:def 4;

hence contradiction by A1, A2; :: thesis: verum

end;then reconsider sp = Support s as non empty Subset of (Bags X) ;

set c = the Element of sp;

s . the Element of sp <> 0. L by POLYNOM1:def 4;

hence contradiction by A1, A2; :: thesis: verum

suppose A3:
s . b <> 0. L
; :: thesis: s is finite-Support

hence s is finite-Support by POLYNOM1:def 5; :: thesis: verum

end;

A4: now :: thesis: for u being object st u in Support s holds

u in {b}

u in {b}

let u be object ; :: thesis: ( u in Support s implies u in {b} )

assume A5: u in Support s ; :: thesis: u in {b}

then reconsider u9 = u as Element of Bags X ;

s . u9 <> 0. L by A5, POLYNOM1:def 4;

then u9 = b by A1;

hence u in {b} by TARSKI:def 1; :: thesis: verum

end;assume A5: u in Support s ; :: thesis: u in {b}

then reconsider u9 = u as Element of Bags X ;

s . u9 <> 0. L by A5, POLYNOM1:def 4;

then u9 = b by A1;

hence u in {b} by TARSKI:def 1; :: thesis: verum

now :: thesis: for u being object st u in {b} holds

u in Support s

then
Support s = {b}
by A4, TARSKI:2;u in Support s

let u be object ; :: thesis: ( u in {b} implies u in Support s )

assume u in {b} ; :: thesis: u in Support s

then A6: u = b by TARSKI:def 1;

then reconsider u9 = u as Element of Bags X by PRE_POLY:def 12;

u9 in Support s by A3, A6, POLYNOM1:def 4;

hence u in Support s ; :: thesis: verum

end;assume u in {b} ; :: thesis: u in Support s

then A6: u = b by TARSKI:def 1;

then reconsider u9 = u as Element of Bags X by PRE_POLY:def 12;

u9 in Support s by A3, A6, POLYNOM1:def 4;

hence u in Support s ; :: thesis: verum

hence s is finite-Support by POLYNOM1:def 5; :: thesis: verum