theorem thXXe: :: FIELD_16:37

for R being non degenerated unital Ring
for S being RingExtension of R
for n being non trivial Nat
for a being Element of S holds
( a is_a_root_of X^ (n,R),S iff a |^ n = a )