for R being Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S st b = a holds
for i being Integer holds i '*' a = i '*' b