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 such that
A1: for b' being bag of st b' <> b holds
s . b' = 0. L by Def4;

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

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

now

assume Support s <> {} ; :: thesis: contradiction
then reconsider sp = Support s as non empty Subset of (Bags X) ;
consider c being Element of sp;
c in Support s ;
then s . c <> 0. L by POLYNOM1:def 9;
hence contradiction by A1, A2; :: thesis: verum

end;

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

end;

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

A4: now

let u be set ; :: thesis: ( u in {b} implies u in Support s )
assume u in {b} ; :: thesis: u in Support s
then A5: u = b by TARSKI:def 1;
then reconsider u' = u as Element of Bags X by POLYNOM1:def 14;
u' in Support s by A3, A5, POLYNOM1:def 9;
hence u in Support s ; :: thesis: verum

end;

now

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

end;

then Support s = {b} by A4, TARSKI:2;
hence s is finite-Support by POLYNOM1:def 10; :: thesis: verum

end;

end;