theorem :: POLYNOM5:16

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 `^ 1 = p