let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F
for x being object holds
( x in the carrier of (FAdj (F,{(sqrt a)})) iff ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z) )
let a be non square Element of F; :: thesis: for x being object holds
( x in the carrier of (FAdj (F,{(sqrt a)})) iff ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z) )
let x be object ; :: thesis: ( x in the carrier of (FAdj (F,{(sqrt a)})) iff ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z) )
H: the carrier of (RAdj (F,{(sqrt a)})) = { (Ext_eval (p,(sqrt a))) where p is Polynomial of F : verum } by FIELD_6:45;

now :: thesis: ( x in FAdj (F,{(sqrt a)}) implies ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z) )

assume x in FAdj (F,{(sqrt a)}) ; :: thesis: ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z)
then x in { (Ext_eval (p,(sqrt a))) where p is Polynomial of F : verum } by H, FIELD_6:56;
then consider p1 being Polynomial of F such that
A: x = Ext_eval (p1,(sqrt a)) ;
set ma = MinPoly ((sqrt a),F);
set p = p1 mod (MinPoly ((sqrt a),F));
B: F is Subring of embField (canHomP (X^2- a)) by FIELD_4:def 1;
C: p1 = ((p1 div (MinPoly ((sqrt a),F))) *' (MinPoly ((sqrt a),F))) + (p1 mod (MinPoly ((sqrt a),F))) by RING_4:4;
D: Ext_eval (p1,(sqrt a)) = (Ext_eval (((p1 div (MinPoly ((sqrt a),F))) *' (MinPoly ((sqrt a),F))),(sqrt a))) + (Ext_eval ((p1 mod (MinPoly ((sqrt a),F))),(sqrt a))) by C, B, ALGNUM_1:15
.= ((Ext_eval ((p1 div (MinPoly ((sqrt a),F))),(sqrt a))) * (Ext_eval ((MinPoly ((sqrt a),F)),(sqrt a)))) + (Ext_eval ((p1 mod (MinPoly ((sqrt a),F))),(sqrt a))) by B, ALGNUM_1:20
.= ((Ext_eval ((p1 div (MinPoly ((sqrt a),F))),(sqrt a))) * (0. (embField (canHomP (X^2- a))))) + (Ext_eval ((p1 mod (MinPoly ((sqrt a),F))),(sqrt a))) by FIELD_6:52
.= Ext_eval ((p1 mod (MinPoly ((sqrt a),F))),(sqrt a)) ;
deg (p1 mod (MinPoly ((sqrt a),F))) < deg (MinPoly ((sqrt a),F)) by FIELD_5:16;
then deg (p1 mod (MinPoly ((sqrt a),F))) < deg (X^2- a) by m30;
then deg (p1 mod (MinPoly ((sqrt a),F))) < 2 by qua4;
then consider y, z being F -membered Element of (FAdj (F,{(sqrt a)})) such that
E: Ext_eval ((p1 mod (MinPoly ((sqrt a),F))),(@ (sqrt a))) = y + ((@ (sqrt a)) * z) by deg2evale;
p1 mod (MinPoly ((sqrt a),F)) is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
then Ext_eval ((p1 mod (MinPoly ((sqrt a),F))),(@ (sqrt a))) = x by A, D, FIELD_7:14;
hence ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z) by E; :: thesis: verum

end;

hence ( x in the carrier of (FAdj (F,{(sqrt a)})) iff ex y, z being F -membered Element of (FAdj (F,{(sqrt a)})) st x = y + ((@ (sqrt a)) * z) ) ; :: thesis: verum