let F be formally_real Field; :: thesis: for E being FieldExtension of F
for a being Element of F
for b being Element of E st b ^2 = a & not FAdj (F,{b}) is formally_real holds
- a in QS F
let E be FieldExtension of F; :: thesis: for a being Element of F
for b being Element of E st b ^2 = a & not FAdj (F,{b}) is formally_real holds
- a in QS F
let a be Element of F; :: thesis: for b being Element of E st b ^2 = a & not FAdj (F,{b}) is formally_real holds
- a in QS F
let b be Element of E; :: thesis: ( b ^2 = a & not FAdj (F,{b}) is formally_real implies - a in QS F )
set P = the Ordering of F;
assume A: ( b ^2 = a & not FAdj (F,{b}) is formally_real ) ; :: thesis: - a in QS F

per cases ( a is square or not a is square ) ;

suppose a is square ; :: thesis: - a in QS F

then consider c being Element of F such that
B: c ^2 = a ;
( b = c or b = - c ) by A, B, FIELD_9:8;
then b in the carrier of F ;
then {b} c= the carrier of F by TARSKI:def 1;
then FAdj (F,{b}) == F by FIELD_7:3;
then FAdj (F,{b}) is ordered by lemPP;
hence - a in QS F by A; :: thesis: verum

end;

suppose B0: not a is square ; :: thesis: - a in QS F

B1: now :: thesis: not b in F

assume b in F ; :: thesis: contradiction
then reconsider c = b as Element of F ;
F is Subring of E by FIELD_4:def 1;
then c ^2 = a by A, FIELD_6:16;
hence contradiction by B0; :: thesis: verum

end;

- (1. (FAdj (F,{b}))) in QS (FAdj (F,{b})) by A, REALALG2:def 3;
then consider c being Element of (FAdj (F,{b})) such that
B2: ( c = - (1. (FAdj (F,{b}))) & c is sum_of_squares ) ;
consider f being FinSequence of (FAdj (F,{b})) such that
B3: ( Sum f = c & ( for i being Nat st i in dom f holds
ex d being Element of (FAdj (F,{b})) st f . i = d ^2 ) ) by B2;
H1: ( F is Subring of E & F is Subring of FAdj (F,{b}) ) by FIELD_4:def 1;
then H2: 1. F = 1. (FAdj (F,{b})) by C0SP1:def 3;

per cases ( f is empty or not f is empty ) ;

suppose f is empty ; :: thesis: - a in QS F

hence - a in QS F by B2, B3; :: thesis: verum

end;

suppose not f is empty ; :: thesis: - a in QS F

then reconsider f = f as non empty FinSequence of (FAdj (F,{b})) ;
for i being Element of dom f holds f . i is square by B3;
then reconsider f = f as non empty quadratic FinSequence of (FAdj (F,{b})) by REALALG2:def 5;
Sum f = - (1. F) by B2, B3, H1, H2, FIELD_6:17;
then Sum f in F ;
then consider g1, g2 being non empty quadratic FinSequence of F such that
B4: Sum f = (Sum g1) + (a * (Sum g2)) by A, B1, maina;

B5: now :: thesis: not Sum g2 is zero

assume Sum g2 is zero ; :: thesis: contradiction
then Sum g1 = - (1. F) by B4, B3, B2, H1, H2, FIELD_6:17;
then ( - (1. F) in QS F & QS F c= the Ordering of F ) by REALALG1:24;
hence contradiction by REALALG1:26; :: thesis: verum

end;

Sum f = - (1. F) by B2, B3, H1, H2, FIELD_6:17;
then (- (1. F)) - (a * (Sum g2)) = (Sum g1) + ((a * (Sum g2)) - (a * (Sum g2))) by B4, RLVECT_1:28
.= (Sum g1) + (0. F) by RLVECT_1:15 ;
then (1. F) + (Sum g1) = ((1. F) + (- (1. F))) - (a * (Sum g2)) by RLVECT_1:def 3
.= (0. F) - (a * (Sum g2)) by RLVECT_1:5
.= (- a) * (Sum g2) by VECTSP_1:9 ;
then ((1. F) + (Sum g1)) * ((Sum g2) ") = (- a) * ((Sum g2) * ((Sum g2) ")) by GROUP_1:def 3
.= (- a) * (1. F) by B5, VECTSP_1:def 10 ;
hence - a in QS F by B5; :: thesis: verum

end;

end;

end;

end;