assume a is F -algebraic ; :: thesis: a " in RAdj (F,{a})
then A1: FAdj (F,{a}) = RAdj (F,{a}) by ch1;
A2: {a} is Subset of (FAdj (F,{a})) by FAt;
a in {a} by TARSKI:def 1;
then reconsider b = a as Element of the carrier of (FAdj (F,{a})) by A2;
b " in the carrier of (FAdj (F,{a})) ;
hence a " in RAdj (F,{a}) by A1, Th19f; :: thesis: verum

assume a " in RAdj (F,{a}) ; :: thesis: a is F -algebraic
then a " in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by lemphi5;
then consider p being Polynomial of F such that
A1: a " = Ext_eval (p,a) ;
set r = (- (1. F)) | F;
set q = ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F);
- (0. F) = 0. F ;
then - (1. F) <> 0. F ;
then B0: deg ((- (1. F)) | F) = 0 by RING_4:21;
B5: deg (rpoly (1,(0. F))) = 1 by HURWITZ:27;
not ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) is zero then reconsider q = ((rpoly (1,(0. F))) *' p) + ((- (1. F)) | F) as non zero Polynomial of F ;
1. E = 1. F by X, C0SP1:def 3;
then A2: - (1. E) = (- (1. F)) * (1. F) by X, Th19
.= (- (1. F)) * (LC (1_. F)) by RATFUNC1:def 7
.= LC ((- (1. F)) * (1_. F)) by RATFUNC1:18
.= LC ((- (1. F)) | F) by RING_4:16 ;
A3: 0. E = 0. F by X, C0SP1:def 3;
reconsider rpE = rpoly (1,(0. E)) as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
reconsider rpF = rpoly (1,(0. F)) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
A5: a <> 0. E ;
Ext_eval (q,a) = (Ext_eval (((rpoly (1,(0. F))) *' p),a)) + (Ext_eval (((- (1. F)) | F),a)) by X, ALGNUM_1:15
.= ((Ext_eval ((rpoly (1,(0. F))),a)) * (a ")) + (Ext_eval (((- (1. F)) | F),a)) by X, A1, ALGNUM_1:20
.= ((Ext_eval (rpF,a)) * (a ")) + (- (1. E)) by A2, exevalconst
.= ((eval (rpE,a)) * (a ")) + (- (1. E)) by A3, FIELD_4:21, FIELD_4:26
.= ((a - (0. E)) * (a ")) + (- (1. E)) by HURWITZ:29
.= ((a ") * a) + (- (1. E)) by GROUP_1:def 12
.= (1. E) + (- (1. E)) by A5, VECTSP_1:def 10
.= 0. E by RLVECT_1:5 ;
hence a is F -algebraic by alg00; :: thesis: verum