theorem Th19: :: POLYNOM5:19

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr
for p being Polynomial of L
for n being Nat holds p `^ (n + 1) = (p `^ n) *' p