set E = embField (canHomP (X^2- a));
A0: F is Subring of embField (canHomP (X^2- a)) by FIELD_4:def 1;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring (embField (canHomP (X^2- a)))) by FIELD_4:10;
then reconsider q = X^2- a as Element of the carrier of (Polynom-Ring (embField (canHomP (X^2- a)))) ;
A1: eval (q,(KrRootP (X^2- a))) = Ext_eval ((X^2- a),(sqrt a)) by FIELD_4:26
.= 0. F by FIELD_5:17 ;

now :: thesis: not sqrt a = 0. (embField (canHomP (X^2- a)))

assume sqrt a = 0. (embField (canHomP (X^2- a))) ; :: thesis: contradiction
then reconsider o = sqrt a as Element of F by A0, C0SP1:def 3;
o is_a_root_of X^2- a by A1, FIELD_4:27;
then X^2- a is with_roots ;
hence contradiction ; :: thesis: verum

end;

hence ( not sqrt a is zero & sqrt a is F -algebraic ) ; :: thesis: verum