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

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

assume a is_a_root_of X^ (n,R),S ; :: thesis: a |^ n = a
then 0. S = Ext_eval ((X^ (n,R)),a) by FIELD_4:def 2
.= (a |^ n) - a by tevale ;
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),S )

assume a |^ n = a ; :: thesis: a is_a_root_of X^ (n,R),S
then 0. S = (a |^ n) - a by RLVECT_1:15
.= Ext_eval ((X^ (n,R)),a) by tevale ;
hence a is_a_root_of X^ (n,R),S by FIELD_4:def 2; :: thesis: verum

end;

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