theorem Th13: :: FIELD_11:34

for F being Field
for i being Nat
for m being Ordinal st m in card (nonConstantPolys F) holds
(power (Polynom-Ring ((card (nonConstantPolys F)),F))) . ((Poly (m,(anpoly ((1. F),1)))),i) = Poly (m,(anpoly ((1. F),i)))