theorem thXX: :: FIELD_16:34

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