let F be ordered Field; :: thesis: for E being FieldExtension of F
for P being Ordering of F holds
( P extends_to E iff for f being non empty b₂ -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial )
let E be FieldExtension of F; :: thesis: for P being Ordering of F holds
( P extends_to E iff for f being non empty b₁ -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial )
let P be Ordering of F; :: thesis: ( P extends_to E iff for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial )

Z: now :: thesis: ( P extends_to E implies for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial )

assume P extends_to E ; :: thesis: for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial
then consider O being Subset of E such that
B0: ( P c= O & O is positive_cone ) ;
reconsider E1 = E as ordered FieldExtension of F by B0, REALALG1:def 17;
reconsider O = O as Ordering of E1 by B0;

now :: thesis: for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial

let f be non empty P -quadratic FinSequence of E; :: thesis: ( Sum f = 0. E implies f is trivial )
assume C0: ( Sum f = 0. E & not f is trivial ) ; :: thesis: contradiction
then Sum f in O \ {(0. E)} by B0, l13, lemB3;
then ( Sum f in O & not Sum f in {(0. E)} ) by XBOOLE_0:def 5;
hence contradiction by C0, TARSKI:def 1; :: thesis: verum

end;

hence for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial ; :: thesis: verum

end;

set g = <*(1. E)*>;
F is Subfield of E by FIELD_4:7;
then A: 1. E = 1. F by EC_PF_1:def 1;
B: dom <*(1. E)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

now :: thesis: for i being Element of NAT st i in dom <*(1. E)*> holds
ex a being non zero Element of E ex b being Element of E st
( a in P & <*(1. E)*> . i = a * (b ^2) )

let i be Element of NAT ; :: thesis: ( i in dom <*(1. E)*> implies ex a being non zero Element of E ex b being Element of E st
( a in P & <*(1. E)*> . i = a * (b ^2) ) )
assume i in dom <*(1. E)*> ; :: thesis: ex a being non zero Element of E ex b being Element of E st
( a in P & <*(1. E)*> . i = a * (b ^2) )
then C: i = 1 by B, TARSKI:def 1;
(1. E) * ((1. E) ^2) = <*(1. E)*> . i by C;
hence ex a being non zero Element of E ex b being Element of E st
( a in P & <*(1. E)*> . i = a * (b ^2) ) by A, REALALG1:25; :: thesis: verum

end;

then reconsider g = <*(1. E)*> as non empty P -quadratic FinSequence of E by dq;

now :: thesis: ( ( for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial ) implies P extends_to E )

assume AS: for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial ; :: thesis: P extends_to E

now :: thesis: not - (1. E) in QS (E,P)

assume - (1. E) in QS (E,P) ; :: thesis: contradiction
then consider h being P -quadratic FinSequence of E such that
C: Sum h = - (1. E) ;
Sum (g ^ h) = (Sum g) + (Sum h) by RLVECT_1:41
.= (1. E) + (- (1. E)) by C, RLVECT_1:44
.= 0. E by RLVECT_1:5 ;
hence contradiction by AS; :: thesis: verum

end;

hence P extends_to E by lemoe2, lemoe4; :: thesis: verum

end;

hence ( P extends_to E iff for f being non empty P -quadratic FinSequence of E st Sum f = 0. E holds
f is trivial ) by Z; :: thesis: verum