theorem Th23: :: POLYNOM7:23

for X being set
for L being non empty ZeroStr
for a being Element of L holds
( term (a | (X,L)) = EmptyBag X & coefficient (a | (X,L)) = a )