let R be non degenerated unital Ring; :: thesis: 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 )
let n be non trivial Nat; :: thesis: for a being Element of R holds
( a is_a_root_of X^ (n,R) iff a |^ n = a )
let a be Element of R; :: thesis: ( a is_a_root_of X^ (n,R) iff a |^ n = a )

A: now :: thesis: ( a is_a_root_of X^ (n,R) implies a |^ n = a )

assume a is_a_root_of X^ (n,R) ; :: thesis: a |^ n = a
then 0. R = (a |^ n) - a by teval;
hence a |^ n = a by RLVECT_1:21; :: thesis: verum

end;

now :: thesis: ( a |^ n = a implies a is_a_root_of X^ (n,R) )

assume a |^ n = a ; :: thesis: a is_a_root_of X^ (n,R)
then 0. R = (a |^ n) - a by RLVECT_1:15
.= eval ((X^ (n,R)),a) by teval ;
hence a is_a_root_of X^ (n,R) ; :: thesis: verum

end;

hence ( a is_a_root_of X^ (n,R) iff a |^ n = a ) by A; :: thesis: verum