theorem Th29: :: POLYNOM9:29

for n being Nat
for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R holds p `^ (n + 1) = (p `^ n) *' p