let F be ordered Field; :: thesis:
let P be Ordering of F; :: thesis:
let E be FieldExtension of F; :: thesis:
let a be non zero Element of E; :: thesis:

now :: thesis:

assume A: a in QS (E,P) ; :: thesis:
consider g being P -quadratic FinSequence of E such that
B: Sum g = a by A;
Z: not g is empty by B;
defpred S₁[ Nat] means for g being non empty P -quadratic FinSequence of E st len g = $1 & Sum g <> 0. E holds
ex f being non empty P -quadratic FinSequence of E st
( Sum f = Sum g & ( for i being Element of NAT st i in dom f holds
f . i <> 0. E ) );
IA: S₁[1]

proof

now :: thesis:

let g be non empty P -quadratic FinSequence of E; :: thesis:
assume A1: ( len g = 1 & Sum g <> 0. E ) ; :: thesis:
set y = g . 1;
A2: g = <*(g . 1)*> by A1, FINSEQ_1:40;
rng <*(g . 1)*> = {(g . 1)} by FINSEQ_1:39;
then g . 1 in rng <*(g . 1)*> by TARSKI:def 1;
then consider u being object such that
A6: ( u in dom g & g . u = g . 1 ) by A2, FUNCT_1:def 3;
reconsider u = u as Element of NAT by A6;
( g . u in rng g & rng g c= the carrier of E ) by A6, FUNCT_1:3;
then reconsider y = g . 1 as Element of the carrier of E by A6;

now :: thesis:

let i be Element of NAT ; :: thesis:
assume H: i in dom g ; :: thesis:
dom g = Seg 1 by A2, FINSEQ_1:38;
then i = 1 by H, FINSEQ_1:2, TARSKI:def 1;
hence g . i <> 0. E by A1, A2, RLVECT_1:44; :: thesis:

end;

hence ex f being non empty P -quadratic FinSequence of E st
( Sum f = Sum g & ( for i being Element of NAT st i in dom f holds
f . i <> 0. E ) ) ; :: thesis:

end;

hence S₁[1] ; :: thesis:

end;

IS: now :: thesis:

let k be Nat; :: thesis:
assume A: k >= 1 ; :: thesis:
assume IV: S₁[k] ; :: thesis:

now :: thesis:

let f be non empty P -quadratic FinSequence of E; :: thesis:
assume A1: ( len f = k + 1 & Sum f <> 0. E ) ; :: thesis:
consider G being FinSequence, y being object such that
A3: f = G ^ <*y*> by FINSEQ_1:46;
A4: len f = (len G) + (len <*y*>) by A3, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
rng G c= rng f by A3, FINSEQ_1:29;
then reconsider G = G as non empty FinSequence of E by A, A1, A4, XBOOLE_1:1, FINSEQ_1:def 4;
rng <*y*> = {y} by FINSEQ_1:39;
then A6: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng f by A3, FINSEQ_1:30;
then consider u being object such that
A7: ( u in dom f & f . u = y ) by A6, FUNCT_1:def 3;
reconsider u = u as Element of NAT by A7;
( f . u in rng f & rng f c= the carrier of E ) by A7, FUNCT_1:3;
then reconsider y = y as Element of the carrier of E by A7;
reconsider g1 = <*y*> as FinSequence of E ;
f = G ^ g1 by A3;
then reconsider G = G, g1 = g1 as non empty P -quadratic FinSequence of E by XYZbS3a;

per cases ;

suppose Sum G = 0. E ; :: thesis:

then I: (0. E) + (Sum g1) = Sum f by A3, RLVECT_1:41;

now :: thesis:

let i be Element of NAT ; :: thesis:
assume H: i in dom g1 ; :: thesis:
dom g1 = Seg 1 by FINSEQ_1:38;
then J: i = 1 by H, FINSEQ_1:2, TARSKI:def 1;
thus g1 . i <> 0. E by J, I, A1, RLVECT_1:44; :: thesis:

end;

hence ex g being non empty P -quadratic FinSequence of E st
( Sum f = Sum g & ( for i being Element of NAT st i in dom g holds
g . i <> 0. E ) ) by I; :: thesis:

end;

suppose Sum G <> 0. E ; :: thesis:

then consider G1 being non empty P -quadratic FinSequence of E such that
B: ( Sum G1 = Sum G & ( for i being Element of NAT st i in dom G1 holds
G1 . i <> 0. E ) ) by A1, A4, IV;
C: Sum f = (Sum G) + (Sum <*y*>) by A3, RLVECT_1:41
.= (Sum G) + y by RLVECT_1:44 ;

per cases ;

suppose y = 0. E ; :: thesis:

hence ex g being non empty P -quadratic FinSequence of E st
( Sum f = Sum g & ( for i being Element of NAT st i in dom g holds
g . i <> 0. E ) ) by B, C; :: thesis:

end;

suppose D1: y <> 0. E ; :: thesis:

set g = G1 ^ g1;
D2: Sum (G1 ^ g1) = (Sum G1) + (Sum <*y*>) by RLVECT_1:41
.= Sum f by B, C, RLVECT_1:44 ;

now :: thesis:

let i be Element of NAT ; :: thesis:
assume D3: i in dom (G1 ^ g1) ; :: thesis:
D4: dom (G1 ^ g1) = Seg (len (G1 ^ g1)) by FINSEQ_1:def 3;
len (G1 ^ g1) = (len G1) + (len g1) by FINSEQ_1:22
.= (len G1) + 1 by FINSEQ_1:39 ;
then D6: ( 1 <= i & i <= (len G1) + 1 ) by D3, D4, FINSEQ_1:1;

per cases ;

suppose D6: i in dom G1 ; :: thesis:

then (G1 ^ g1) . i = G1 . i by FINSEQ_1:def 7;
hence (G1 ^ g1) . i <> 0. E by B, D6; :: thesis:

end;

suppose D7: not i in dom G1 ; :: thesis:

D8: now :: thesis:

assume i <> (len G1) + 1 ; :: thesis:
then i < (len G1) + 1 by D6, XXREAL_0:1;
then (i + 1) - 1 <= ((len G1) + 1) - 1 by INT_1:7;
then i in Seg (len G1) by D6, FINSEQ_1:1;
hence contradiction by D7, FINSEQ_1:def 3; :: thesis:

end;

dom g1 = Seg 1 by FINSEQ_1:38;
then 1 in dom g1 by FINSEQ_1:3;
then (G1 ^ g1) . i = g1 . 1 by D8, FINSEQ_1:def 7
.= y ;
hence (G1 ^ g1) . i <> 0. E by D1; :: thesis:

end;

hence ex g being non empty P -quadratic FinSequence of E st
( Sum f = Sum g & ( for i being Element of NAT st i in dom g holds
g . i <> 0. E ) ) by D2; :: thesis:

end;

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

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(IA, IS);
consider n being Nat such that
H: len g = n ;
n >= 0 + 1 by Z, H, INT_1:7;
hence ex f being non empty P -quadratic FinSequence of E st
( Sum f = a & ( for i being Element of NAT st i in dom f holds
f . i <> 0. E ) ) by Z, H, I, B; :: thesis:

end;

hence ( a in QS (E,P) iff ex f being non empty P -quadratic FinSequence of E st
( Sum f = a & ( for i being Element of NAT st i in dom f holds
f . i <> 0. E ) ) ) ; :: thesis: