:: deftheorem defines 0_ POLYNOM1:def 8 :
for n being set
for S being non empty ZeroStr holds 0_ (n,S) = (Bags n) --> (0. S);