let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds (sqrt a) * (sqrt a) = a
let a be non square Element of F; :: thesis: (sqrt a) * (sqrt a) = a
B: 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))) ;
H: ( - a = - b & 0. F = 0. (embField (canHomP (X^2- a))) & 1. F = 1. (embField (canHomP (X^2- a))) ) by FIELD_6:17, B, C0SP1:def 3;
0. (embField (canHomP (X^2- a))) = 0. F by B, C0SP1:def 3
.= Ext_eval ((X^2- a),(sqrt a)) by FIELD_5:17
.= eval ((X^2- b),(sqrt a)) by H, FIELD_4:26
.= ((- b) + ((0. (embField (canHomP (X^2- a)))) * (sqrt a))) + ((1. (embField (canHomP (X^2- a)))) * ((sqrt a) ^2)) by evalq
.= ((sqrt a) * (sqrt a)) - b by O_RING_1:def 1 ;
hence (sqrt a) * (sqrt a) = a by RLVECT_1:21; :: thesis: verum