let F be non 2 -characteristic Field; :: thesis: for a being Element of F holds
( X^2- a is reducible iff a is square )
let a be Element of F; :: thesis: ( X^2- a is reducible iff a is square )
H: ( 2 '*' (1. F) <> 0. F & 4 '*' (1. F) <> 0. F ) by ch2, ch4;

B: now :: thesis: ( X^2- a is reducible implies a is square )

assume X^2- a is reducible ; :: thesis: a is square
then DC <%(- a),(0. F),(1. F)%> is square by naH;
then - (4 '*' (- a)) is square by defDCpq;
then 4 '*' (- (- a)) is square by REALALG2:6;
then consider w being Element of F such that
C: w ^2 = 4 '*' a by O_RING_1:def 2;
w * w = 4 '*' ((1. F) * a) by C, O_RING_1:def 1
.= (4 '*' (1. F)) * a by REALALG2:5
.= a * (4 '*' (1. F)) by GROUP_1:def 12 ;
then (w * w) * ((4 '*' (1. F)) ") = a * ((4 '*' (1. F)) * ((4 '*' (1. F)) ")) by GROUP_1:def 3
.= a * (((4 '*' (1. F)) ") * (4 '*' (1. F))) by GROUP_1:def 12
.= a * (1. F) by H, VECTSP_1:def 10 ;
then a = (w * w) * (((2 * 2) '*' (1. F)) ")
.= (w * w) * (((2 '*' (1. F)) * (2 '*' (1. F))) ") by RING_3:67
.= (w * w) * (((2 '*' (1. F)) ") * ((2 '*' (1. F)) ")) by H, VECTSP_2:11
.= w * (w * (((2 '*' (1. F)) ") * ((2 '*' (1. F)) "))) by GROUP_1:def 3
.= w * ((w * ((2 '*' (1. F)) ")) * ((2 '*' (1. F)) ")) by GROUP_1:def 3
.= w * (((2 '*' (1. F)) ") * (w * ((2 '*' (1. F)) "))) by GROUP_1:def 12
.= (w * ((2 '*' (1. F)) ")) * (w * ((2 '*' (1. F)) ")) by GROUP_1:def 3
.= (w * ((2 '*' (1. F)) ")) ^2 by O_RING_1:def 1 ;
hence a is square ; :: thesis: verum

end;

now :: thesis: ( a is square implies X^2- a is reducible )

assume a is square ; :: thesis: X^2- a is reducible
then consider w being Element of F such that
C: w ^2 = a by O_RING_1:def 2;
(2 '*' w) ^2 = (2 '*' w) * (2 '*' w) by O_RING_1:def 1
.= 2 '*' (w * (2 '*' w)) by REALALG2:5
.= 2 '*' ((2 '*' w) * w) by GROUP_1:def 12
.= 2 '*' (2 '*' (w * w)) by REALALG2:5
.= (2 * 2) '*' (w * w) by RING_3:65
.= 4 '*' a by C, O_RING_1:def 1 ;
then 4 '*' (- (- a)) is square ;
then - (4 '*' (- a)) is square by REALALG2:6;
then DC <%(- a),(0. F),(1. F)%> is square by defDCpq;
hence X^2- a is reducible by naH; :: thesis: verum

end;

hence ( X^2- a is reducible iff a is square ) by B; :: thesis: verum