theorem Th3: :: FIELD_1:2

for R being Ring
for I being Ideal of R
for x being Element of (R / I)
for a being Element of R st x = Class ((EqRel (R,I)),a) holds
for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n))