let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds Roots ((FAdj (F,{(sqrt a)})),(X^2- a)) = {(sqrt a),(- (sqrt a))}
let a be non square Element of F; :: thesis: Roots ((FAdj (F,{(sqrt a)})),(X^2- a)) = {(sqrt a),(- (sqrt a))}
set E = FAdj (F,{(sqrt a)});
reconsider p = X^2- a as Element of the carrier of (Polynom-Ring F) ;
reconsider b = sqrt a as Element of (FAdj (F,{(sqrt a)})) by FIELD_7:def 5;
reconsider q = (rpoly (1,b)) *' (rpoly (1,(- b))) as Element of the carrier of (Polynom-Ring (FAdj (F,{(sqrt a)}))) by POLYNOM3:def 10;
H: FAdj (F,{(sqrt a)}) is Subring of embField (canHomP (X^2- a)) by FIELD_4:def 1;
then H1: - b = - (sqrt a) by FIELD_6:17;
( Roots (rpoly (1,b)) = {b} & Roots (rpoly (1,(- b))) = {(- b)} ) by RING_5:18;
then A: Roots ((rpoly (1,b)) *' (rpoly (1,(- b)))) = {b} \/ {(- b)} by UPROOTS:23
.= {b,(- b)} by ENUMSET1:1 ;
I: X- b = X- (sqrt a) by FIELD_4:21;
K: X+ b = X+ (sqrt a) by H1, FIELD_4:21;
(rpoly (1,b)) *' (rpoly (1,(- b))) = (X- (sqrt a)) *' (X+ (sqrt a)) by I, K, FIELD_4:17
.= X^2- a by Fi1a ;
then Roots ((FAdj (F,{(sqrt a)})),p) = Roots q by FIELD_7:13;
hence Roots ((FAdj (F,{(sqrt a)})),(X^2- a)) = {(sqrt a),(- (sqrt a))} by A, H, FIELD_6:17; :: thesis: verum