let F be Field; :: thesis: for n being non zero Nat
for a, b being Element of F holds
( b is_a_root_of X^ (n,a) iff b |^ n = a )
let n be non zero Nat; :: thesis: for a, b being Element of F holds
( b is_a_root_of X^ (n,a) iff b |^ n = a )
let a, b be Element of F; :: thesis: ( b is_a_root_of X^ (n,a) iff b |^ n = a )

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

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

end;

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

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

end;

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