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 ) by FUNCOP_1:7;
then Support P = {} (Bags n) by Def9;
hence Support P is finite ; :: according to POLYNOM1:def 4 :: thesis: verum