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)
for a being non zero Element of (FAdj (F,{(sqrt (DC p))}))
for b, c being Element of (FAdj (F,{(sqrt (DC p))})) st p = <%c,b,a%> holds
( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") )
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F); :: thesis: for a being non zero Element of (FAdj (F,{(sqrt (DC p))}))
for b, c being Element of (FAdj (F,{(sqrt (DC p))})) st p = <%c,b,a%> holds
( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") )
let a be non zero Element of (FAdj (F,{(sqrt (DC p))})); :: thesis: for b, c being Element of (FAdj (F,{(sqrt (DC p))})) st p = <%c,b,a%> holds
( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") )
let b, c be Element of (FAdj (F,{(sqrt (DC p))})); :: thesis: ( p = <%c,b,a%> implies ( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") ) )
reconsider E = FAdj (F,{(sqrt (DC p))}) as F -extending FieldExtension of F by FIELD_4:6;
assume p = <%c,b,a%> ; :: thesis: ( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") )
then H: ( p . 1 = b & p . 2 = a ) by qua1;
A: ( @ (b,E) = b & @ (a,E) = a ) by FIELD_7:def 4;
then @ (b,E) = @ ((p . 1),E) by H, FIELD_7:def 4;
hence ( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") ) by A, H, FIELD_7:def 4; :: thesis: verum