theorem multi0: :: FIELD_14:19

for F being Field
for p being Polynomial of F
for i, j being Element of NAT holds p `^ (i + j) = (p `^ i) *' (p `^ j)