theorem :: POLYNOM5:18

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