theorem Th11: :: FIELD_11:32

for F being Field
for a being non zero Element of F
for i being Nat
for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i)))