theorem ZZZ: :: FIELD_11:25

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being constant Polynomial of F holds
( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 )