theorem Xm: :: FIELD_16:41

for n being non trivial Nat
for R being Ring
for S being RingExtension of R holds X^ (n,R) = X^ (n,S)