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 (RootDC p) * (RootDC p) = DC p
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F); :: thesis: (RootDC p) * (RootDC p) = DC p
A: FAdj (F,{(sqrt (DC p))}) is Subring of embField (canHomP (X^2- (DC p))) by FIELD_4:def 1;
thus (RootDC p) * (RootDC p) = (sqrt (DC p)) * (sqrt (DC p)) by A, FIELD_6:16
.= DC p by m1 ; :: thesis: verum