theorem Th13a: :: FIELD_11:33

for F being Field
for i being Element of NAT
for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1))))