let F be ordered Field; :: thesis: for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E st O extends P holds
QS (E,P) c= O
let E be ordered FieldExtension of F; :: thesis: for P being Ordering of F
for O being Ordering of E st O extends P holds
QS (E,P) c= O
let P be Ordering of F; :: thesis: for O being Ordering of E st O extends P holds
QS (E,P) c= O
let O be Ordering of E; :: thesis: ( O extends P implies QS (E,P) c= O )
assume O extends P ; :: thesis: QS (E,P) c= O
then AS: P c= O by l13;
defpred S₁[ Nat] means for f being P -quadratic FinSequence of E st len f = $1 holds
Sum f in O;
I: F is Subfield of E by FIELD_4:7;

now :: thesis: for f being P -quadratic FinSequence of E st len f = 0 holds
Sum f in O

let f be P -quadratic FinSequence of E; :: thesis: ( len f = 0 implies Sum f in O )
assume len f = 0 ; :: thesis: Sum f in O
then f = <*> the carrier of E ;
then Sum f = 0. E by RLVECT_1:43
.= 0. F by I, EC_PF_1:def 1 ;
hence Sum f in O by AS, REALALG1:25; :: thesis: verum

end;

then I0: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being P -quadratic FinSequence of E st len f = k + 1 holds
Sum f in O

let f be P -quadratic FinSequence of E; :: thesis: ( len f = k + 1 implies Sum b₁ in O )
assume B0: len f = k + 1 ; :: thesis: Sum b₁ in O
then f <> {} ;
then consider h being FinSequence, x being object such that
B1: f = h ^ <*x*> by FINSEQ_1:46;
reconsider f1 = f as non empty P -quadratic FinSequence of E by B0;

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

suppose h is empty ; :: thesis: Sum b₁ in O

then B0: f = <*x*> by B1, FINSEQ_1:34;
then dom f = {1} by FINSEQ_1:2, FINSEQ_1:38;
then B2: 1 in dom f by TARSKI:def 1;
then B5: ( f . 1 in rng f & f . 1 = x ) by B0, FUNCT_1:3;
then reconsider x = x as Element of E ;
consider a being non zero Element of E, b being Element of E such that
B3: ( a in P & f . 1 = a * (b ^2) ) by B2, dq;
B4: Sum f = x by B0, RLVECT_1:44;
( a in O & b ^2 in O ) by B3, AS, REALALG1:23;
hence Sum f in O by B3, B4, B5, REALALG1:def 5; :: thesis: verum

end;

suppose not h is empty ; :: thesis: Sum b₁ in O

then reconsider h = h as non empty FinSequence of E by B1, FINSEQ_1:36;
reconsider r = <*x*> as non empty FinSequence of E by B1, FINSEQ_1:36;
len r = 1 by FINSEQ_1:39;
then B2: len f = (len h) + 1 by B1, FINSEQ_1:22;
dom r = {1} by FINSEQ_1:2, FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then ( r . 1 in rng r & r . 1 = x ) by FUNCT_1:3;
then reconsider x = x as Element of E ;
f1 = h ^ r by B1;
then reconsider h = h, r = r as P -quadratic FinSequence of E by XYZbS3a;
B3: Sum r in O

proof

dom r = {1} by FINSEQ_1:2, FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then consider a being non zero Element of E, b being Element of E such that
B3: ( a in P & r . 1 = a * (b ^2) ) by dq;
B4: Sum r = x by RLVECT_1:44;
( a in O & b ^2 in O ) by B3, AS, REALALG1:23;
hence Sum r in O by B3, B4, REALALG1:def 5; :: thesis: verum

end;

Sum h in O by IV, B0, B2;
then (Sum r) + (Sum h) in O by B3, IDEAL_1:def 1;
hence Sum f in O by B1, RLVECT_1:41; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(I0, IS);

now :: thesis: for o being object st o in QS (E,P) holds
o in O

let o be object ; :: thesis: ( o in QS (E,P) implies o in O )
assume o in QS (E,P) ; :: thesis: o in O
then consider f being P -quadratic FinSequence of E such that
A: Sum f = o ;
consider n being Nat such that
H: len f = n ;
thus o in O by H, A, I; :: thesis: verum

end;

hence QS (E,P) c= O ; :: thesis: verum