let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds (X- (sqrt a)) *' (X+ (sqrt a)) = X^2- a
let a be non square Element of F; :: thesis: (X- (sqrt a)) *' (X+ (sqrt a)) = X^2- a
set E = embField (canHomP (X^2- a));
H: F is Subring of embField (canHomP (X^2- a)) by FIELD_4:def 1;
then the carrier of F c= the carrier of (embField (canHomP (X^2- a))) by C0SP1:def 3;
then reconsider b = a as Element of (embField (canHomP (X^2- a))) ;
A: (sqrt a) * (- (sqrt a)) = - ((sqrt a) * (sqrt a)) by VECTSP_1:8
.= - b by m1 ;
- ((sqrt a) + (- (sqrt a))) = - (0. (embField (canHomP (X^2- a)))) by RLVECT_1:5
.= 0. (embField (canHomP (X^2- a))) ;
then B: (X- (sqrt a)) *' (X- (- (sqrt a))) = <%(- b),(0. (embField (canHomP (X^2- a)))),(1. (embField (canHomP (X^2- a))))%> by A, lemred3z;
( 0. (embField (canHomP (X^2- a))) = 0. F & 1. (embField (canHomP (X^2- a))) = 1. F ) by H, C0SP1:def 3;
hence (X- (sqrt a)) *' (X+ (sqrt a)) = X^2- a by B, H, FIELD_6:17; :: thesis: verum