let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds Roots ((FAdj (F,{(sqrt (DC p))})),p) = {(Root1 p),(Root2 p)}
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F); :: thesis: Roots ((FAdj (F,{(sqrt (DC p))})),p) = {(Root1 p),(Root2 p)}
set E = FAdj (F,{(sqrt (DC p))});
set r1 = Root1 p;
set r2 = Root2 p;
reconsider q = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p))) as Element of the carrier of (Polynom-Ring (FAdj (F,{(sqrt (DC p))}))) by POLYNOM3:def 10;
K: F is Subring of FAdj (F,{(sqrt (DC p))}) by FIELD_4:def 1;
Y: Roots ((FAdj (F,{(sqrt (DC p))})),p) = Roots q by Z5, FIELD_7:13;

Z: now :: thesis: not @ ((LC p),(FAdj (F,{(sqrt (DC p))}))) is zero

assume Y1: @ ((LC p),(FAdj (F,{(sqrt (DC p))}))) is zero ; :: thesis: contradiction
LC p = @ ((LC p),(FAdj (F,{(sqrt (DC p))}))) by FIELD_7:def 4
.= 0. F by Y1, K, C0SP1:def 3 ;
hence contradiction ; :: thesis: verum

end;

( Roots (rpoly (1,(Root1 p))) = {(Root1 p)} & Roots (rpoly (1,(Root2 p))) = {(Root2 p)} ) by RING_5:18;
then Roots ((rpoly (1,(Root1 p))) *' (rpoly (1,(Root2 p)))) = {(Root1 p)} \/ {(Root2 p)} by UPROOTS:23
.= {(Root1 p),(Root2 p)} by ENUMSET1:1 ;
hence Roots ((FAdj (F,{(sqrt (DC p))})),p) = {(Root1 p),(Root2 p)} by Y, Z, RING_5:19; :: thesis: verum