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 Root1 p <> Root2 p
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F); :: thesis: Root1 p <> Root2 p
set E = FAdj (F,{(sqrt (DC p))});
set w = RootDC p;
consider a1 being non zero Element of F, b1, c1 being Element of F such that
A: p = <%c1,b1,a1%> by qua5;
set a = @ (a1,(FAdj (F,{(sqrt (DC p))})));
set b = @ (b1,(FAdj (F,{(sqrt (DC p))})));
set c = @ (c1,(FAdj (F,{(sqrt (DC p))})));
I: ( @ (a1,(FAdj (F,{(sqrt (DC p))}))) = a1 & @ (b1,(FAdj (F,{(sqrt (DC p))}))) = b1 & @ (c1,(FAdj (F,{(sqrt (DC p))}))) = c1 ) by FIELD_7:def 4;
then B: p = <%(@ (c1,(FAdj (F,{(sqrt (DC p))})))),(@ (b1,(FAdj (F,{(sqrt (DC p))})))),(@ (a1,(FAdj (F,{(sqrt (DC p))}))))%> by A, eval2;
J: FAdj (F,{(sqrt (DC p))}) is Subring of embField (canHomP (X^2- (DC p))) by FIELD_4:def 1;
K: F is Subring of FAdj (F,{(sqrt (DC p))}) by FIELD_4:def 1;
E: not @ (a1,(FAdj (F,{(sqrt (DC p))}))) is zero by I, K, C0SP1:def 3;
M: not FAdj (F,{(sqrt (DC p))}) is 2 -characteristic by K;
then L: 2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))})))) <> 0. (FAdj (F,{(sqrt (DC p))})) by E, ch2;

now :: thesis: not Root1 p = Root2 p

assume Root1 p = Root2 p ; :: thesis: contradiction
then ((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))}))))) ") = Root2 p by E, B, Z2
.= ((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * ((2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))}))))) ") by E, B, Z2 ;
then (((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))}))))) ")) * (2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))}))))) = ((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * (((2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))}))))) ") * (2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))})))))) by GROUP_1:def 3
.= ((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * (1. (FAdj (F,{(sqrt (DC p))}))) by L, VECTSP_1:def 10 ;
then (- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p) = ((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * (((2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))}))))) ") * (2 '*' (@ (a1,(FAdj (F,{(sqrt (DC p))})))))) by GROUP_1:def 3
.= ((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * (1. (FAdj (F,{(sqrt (DC p))}))) by L, VECTSP_1:def 10 ;
then (@ (b1,(FAdj (F,{(sqrt (DC p))})))) + ((- (@ (b1,(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) = ((@ (b1,(FAdj (F,{(sqrt (DC p))})))) + (- (@ (b1,(FAdj (F,{(sqrt (DC p))})))))) + (RootDC p) by RLVECT_1:def 3
.= (0. (FAdj (F,{(sqrt (DC p))}))) + (RootDC p) by RLVECT_1:5 ;
then RootDC p = ((@ (b1,(FAdj (F,{(sqrt (DC p))})))) + (- (@ (b1,(FAdj (F,{(sqrt (DC p))})))))) + (- (RootDC p)) by RLVECT_1:def 3
.= (0. (FAdj (F,{(sqrt (DC p))}))) + (- (RootDC p)) by RLVECT_1:5 ;
then (RootDC p) + (RootDC p) = 0. (FAdj (F,{(sqrt (DC p))})) by RLVECT_1:5;
then 2 '*' (RootDC p) = 0. (FAdj (F,{(sqrt (DC p))})) by RING_5:2;
then RootDC p = 0. (FAdj (F,{(sqrt (DC p))})) by M, ch2
.= 0. (embField (canHomP (X^2- (DC p)))) by J, C0SP1:def 3 ;
hence contradiction ; :: thesis: verum

end;

hence Root1 p <> Root2 p ; :: thesis: verum