theorem bij3a: :: FIELD_11:23

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being non zero Element of the carrier of (Polynom-Ring F) holds
( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} iff p is constant )