for R being comRing
for S being comRingExtension of R
for x1, x2 being Element of S
for y1, y2 being Element of R
for n being Element of NAT st x1 = y1 & x2 = y2 holds
<%x1,x2%> `^ n = <%y1,y2%> `^ n