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 ;

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

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

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

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

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

end;

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

A4: now :: thesis: for u being object st u in Support s holds
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;

now :: thesis: for u being object st u in {b} holds
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;

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

end;

end;