theorem Th10: :: GROEB_3:10

for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L holds card (Support p) = card (Support (m *' p))