for S being Ring
for R being Subring of S
for x being Element of S
for x1 being Element of R
for n being Element of NAT st x = x1 holds
x |^ n = x1 |^ n