:: deftheorem defines | GROEB_3:def 1 :
for X being set
for L being non empty ZeroStr
for s being Series of X,L
for Y being Subset of (Bags X) holds s | Y = s +* (((Support s) \ Y) --> (0. L));