theorem Th4: :: E_TRANS2:3

for f being Element of the carrier of (Polynom-Ring INT.Ring)
for n being Nat holds ^ (f |^ n) = (^ f) |^ n