reconsider P = (Bags n) --> (0. S) as Function of (Bags n), the carrier of S ;
reconsider P = P as Function of (Bags n),S ;
reconsider P = P as Series of n,S ;
take P ; :: thesis: P is finite-Support
for x being Element of Bags n holds
( x in {} iff P . x <> 0. S ) ;
then Support P = {} (Bags n) by Def4;
hence Support P is finite ; :: according to POLYNOM1:def 5 :: thesis: verum