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
for f being non empty b₂ -quadratic FinSequence of E st not f is trivial holds
Sum f in O \ {(0. E)}
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
for f being non empty b₁ -quadratic FinSequence of E st not f is trivial holds
Sum f in O \ {(0. E)}
let P be Ordering of F; :: thesis: for O being Ordering of E st O extends P holds
for f being non empty P -quadratic FinSequence of E st not f is trivial holds
Sum f in O \ {(0. E)}
let O be Ordering of E; :: thesis: ( O extends P implies for f being non empty P -quadratic FinSequence of E st not f is trivial holds
Sum f in O \ {(0. E)} )
assume AS1: O extends P ; :: thesis: for f being non empty P -quadratic FinSequence of E st not f is trivial holds
Sum f in O \ {(0. E)}
let f be non empty P -quadratic FinSequence of E; :: thesis: ( not f is trivial implies Sum f in O \ {(0. E)} )
assume AS2: not f is trivial ; :: thesis: Sum f in O \ {(0. E)}
H1: QS (E,P) c= O by AS1, lemoe3;
H2: ( O + (O ^+) c= O ^+ & (O ^+) + O c= O ^+ ) by lemP;
defpred S₁[ Nat] means for f being non empty P -quadratic FinSequence of E st not f is trivial & len f = $1 holds
Sum f in O \ {(0. E)};

A: now :: thesis: for f being non empty P -quadratic FinSequence of E st not f is trivial & len f = 1 holds
Sum f in O \ {(0. E)}

let f be non empty P -quadratic FinSequence of E; :: thesis: ( not f is trivial & len f = 1 implies Sum f in O \ {(0. E)} )
assume A0: ( not f is trivial & len f = 1 ) ; :: thesis: Sum f in O \ {(0. E)}
then A1: f = <*(f . 1)*> by FINSEQ_1:40;
then A2: dom f = {1} by FINSEQ_1:2, FINSEQ_1:38;
then 1 in dom f by TARSKI:def 1;
then A3: f . 1 in rng f by FUNCT_1:3;
A5: Sum f in QS (E,P) ;

now :: thesis: not f . 1 = 0. E

assume f . 1 = 0. E ; :: thesis: contradiction
then for i being object st i in dom f holds
f . i = 0. E by A2, TARSKI:def 1;
hence contradiction by A0, REALALG2:def 4; :: thesis: verum

end;

then Sum f <> 0. E by A1, A3, RLVECT_1:44;
then not Sum f in {(0. E)} by TARSKI:def 1;
hence Sum f in O \ {(0. E)} by A5, H1, XBOOLE_0:def 5; :: thesis: verum

end;

then IA: S₁[1] ;

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

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume k >= 1 ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume AS2: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being non empty P -quadratic FinSequence of E st not f is trivial & len f = k + 1 holds
Sum f in O \ {(0. E)}

let f be non empty P -quadratic FinSequence of E; :: thesis: ( not f is trivial & len f = k + 1 implies Sum b₁ in O \ {(0. E)} )
assume AS3: ( not f is trivial & len f = k + 1 ) ; :: thesis: Sum b₁ in O \ {(0. E)}
consider h being FinSequence, x being object such that
B1: f = h ^ <*x*> by FINSEQ_1:46;
reconsider h = h as FinSequence of E by B1, FINSEQ_1:36;
reconsider r = <*x*> as non empty FinSequence of E by B1, FINSEQ_1:36;
f = h ^ r by B1;
then reconsider h = h, r = r as P -quadratic FinSequence of E by XYZbS3a;
len r = 1 by FINSEQ_1:39;
then B2: len f = (len h) + 1 by B1, FINSEQ_1:22;

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

suppose C0: h is trivial ; :: thesis: Sum b₁ in O \ {(0. E)}

then Sum h = 0. E by STRUCT_0:def 12;
then C1: Sum h in O by REALALG1:25;
( not r is trivial & len r = 1 ) by C0, B1, AS3, FINSEQ_1:40;
then Sum r in O \ {(0. E)} by A;
then C2: (Sum h) + (Sum r) in O + (O \ {(0. E)}) by C1;
Sum f = (Sum h) + (Sum r) by B1, RLVECT_1:41;
hence Sum f in O \ {(0. E)} by C2, H2; :: thesis: verum

end;

suppose C0: not h is trivial ; :: thesis: Sum b₁ in O \ {(0. E)}

then not h is empty ;
then C1: Sum h in O \ {(0. E)} by B2, C0, AS2, AS3;
Sum r in QS (E,P) ;
then C2: (Sum h) + (Sum r) in (O \ {(0. E)}) + O by H1, C1;
Sum f = (Sum h) + (Sum r) by B1, RLVECT_1:41;
hence Sum f in O \ {(0. E)} by C2, H2; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(IA, IS);
(len f) + 1 > 0 + 1 by XREAL_1:6;
then len f >= 1 by NAT_1:13;
hence Sum f in O \ {(0. E)} by AS2, I; :: thesis: verum