theorem Th37: :: RINGDER1:37

for R being domRing
for x being Element of (Polynom-Ring R)
for f being Polynomial of R st x = f holds
for n being Nat holds x |^ n = f `^ n