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 p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p)))
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F); :: thesis: p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p)))
set E = FAdj (F,{(sqrt (DC p))});
K: F is Subring of FAdj (F,{(sqrt (DC p))}) by FIELD_4:def 1;
then H: not FAdj (F,{(sqrt (DC p))}) is 2 -characteristic ;
consider a being non zero Element of F, b, c being Element of F such that
A: p = <%c,b,a%> by qua5;
I: ( @ (c,(FAdj (F,{(sqrt (DC p))}))) = c & @ (b,(FAdj (F,{(sqrt (DC p))}))) = b & @ (a,(FAdj (F,{(sqrt (DC p))}))) = a ) by FIELD_7:def 4;
then B: p = <%(@ (c,(FAdj (F,{(sqrt (DC p))})))),(@ (b,(FAdj (F,{(sqrt (DC p))})))),(@ (a,(FAdj (F,{(sqrt (DC p))}))))%> by A, eval2;

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

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

end;

C: Root1 p = ((- (@ (b,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) ") by E, B, Z2;
D: Root2 p = ((- (@ (b,(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * ((2 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) ") by E, B, Z2;
J: (RootDC p) ^2 = (RootDC p) * (RootDC p) by O_RING_1:def 1
.= DC p by Z1
.= (b ^2) - ((4 '*' a) * c) by A, defDC ;
J1: b ^2 = b * b by O_RING_1:def 1
.= (@ (b,(FAdj (F,{(sqrt (DC p))})))) * (@ (b,(FAdj (F,{(sqrt (DC p))})))) by I, K, FIELD_6:16
.= (@ (b,(FAdj (F,{(sqrt (DC p))})))) ^2 by O_RING_1:def 1 ;
(4 '*' a) * c = 4 '*' (a * c) by REALALG2:5
.= 4 '*' ((@ (a,(FAdj (F,{(sqrt (DC p))})))) * (@ (c,(FAdj (F,{(sqrt (DC p))}))))) by Z3, I, K, FIELD_6:16
.= (4 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) * (@ (c,(FAdj (F,{(sqrt (DC p))})))) by REALALG2:5 ;
then - ((4 '*' a) * c) = - ((4 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) * (@ (c,(FAdj (F,{(sqrt (DC p))}))))) by K, FIELD_6:17;
then F: (b ^2) - ((4 '*' a) * c) = ((@ (b,(FAdj (F,{(sqrt (DC p))})))) ^2) - ((4 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) * (@ (c,(FAdj (F,{(sqrt (DC p))}))))) by K, J1, FIELD_6:15;
len p = 3 by A, qua3;
then G: (len p) -' 1 = 3 - 1 by XREAL_0:def 2;
@ (a,(FAdj (F,{(sqrt (DC p))}))) = a by FIELD_7:def 4
.= p . 2 by A, qua1
.= LC p by G, RATFUNC1:def 6
.= @ ((LC p),(FAdj (F,{(sqrt (DC p))}))) by FIELD_7:def 4 ;
hence p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p))) by F, J, H, E, D, C, B, lemred; :: thesis: verum