let F be ordered Field; :: thesis: for E being FieldExtension of F
for P being Ordering of F
for f being FinSequence of E st ( for i being Nat st i in dom f holds
f . i in P ) holds
Sum f in P
let E be FieldExtension of F; :: thesis: for P being Ordering of F
for f being FinSequence of E st ( for i being Nat st i in dom f holds
f . i in P ) holds
Sum f in P
let P be Ordering of F; :: thesis: for f being FinSequence of E st ( for i being Nat st i in dom f holds
f . i in P ) holds
Sum f in P
let f be FinSequence of E; :: thesis: ( ( for i being Nat st i in dom f holds
f . i in P ) implies Sum f in P )
assume AS: for i being Nat st i in dom f holds
f . i in P ; :: thesis: Sum f in P
I1: F is Subring of E by FIELD_4:def 1;
defpred S₁[ Nat] means for f being FinSequence of E st len f = $1 & ( for i being Nat st i in dom f holds
f . i in P ) holds
Sum f in P;
IA: S₁[ 0 ]

proof

now :: thesis: for f being FinSequence of E st len f = 0 & ( for i being Nat st i in dom f holds
f . i in P ) holds
Sum f in P

let f be FinSequence of E; :: thesis: ( len f = 0 & ( for i being Nat st i in dom f holds
f . i in P ) implies Sum f in P )
assume ( len f = 0 & ( for i being Nat st i in dom f holds
f . i in P ) ) ; :: thesis: Sum f in P
then f = <*> the carrier of F ;
then Sum f = Sum (<*> the carrier of F) by I1, FIELD_4:2
.= 0. F by RLVECT_1:43 ;
hence Sum f in P by REALALG1:25; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

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 FinSequence of E st len f = k + 1 & ( for i being Nat st i in dom f holds
f . i in P ) holds
Sum f in P

let f be FinSequence of E; :: thesis: ( len f = k + 1 & ( for i being Nat st i in dom f holds
f . i in P ) implies Sum f in P )
assume AS: ( len f = k + 1 & ( for i being Nat st i in dom f holds
f . i in P ) ) ; :: thesis: Sum f in P
then f <> {} ;
then consider G being FinSequence, y being object such that
B2: f = G ^ <*y*> by FINSEQ_1:46;
rng G c= rng f by B2, FINSEQ_1:29;
then reconsider G = G as FinSequence of E by XBOOLE_1:1, FINSEQ_1:def 4;
B10: len f = (len G) + (len <*y*>) by B2, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
C: dom G c= dom f by B2, FINSEQ_1:26;

D: now :: thesis: for i being Nat st i in dom G holds
G . i in P

let i be Nat; :: thesis: ( i in dom G implies G . i in P )
assume C0: i in dom G ; :: thesis: G . i in P
then G . i = f . i by B2, FINSEQ_1:def 7;
hence G . i in P by C, C0, AS; :: thesis: verum

end;

E: now :: thesis: for o being object st o in rng G holds
o in P

let o be object ; :: thesis: ( o in rng G implies o in P )
assume o in rng G ; :: thesis: o in P
then consider u being object such that
D1: ( u in dom G & G . u = o ) by FUNCT_1:def 3;
reconsider u = u as Element of NAT by D1;
thus o in P by D, D1; :: thesis: verum

end;

rng <*y*> = {y} by FINSEQ_1:39;
then G5: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng f by B2, FINSEQ_1:30;
then consider u being object such that
G6: ( u in dom f & f . u = y ) by G5, FUNCT_1:def 3;
reconsider u = u as Element of NAT by G6;
G7: f . u in P by AS, G6;
then reconsider y1 = y as Element of F by G6;
the carrier of F c= the carrier of E by I1, C0SP1:def 3;
then reconsider y = y as Element of E by G6, G7;

now :: thesis: for o being object st o in rng G holds
o in the carrier of F

let o be object ; :: thesis: ( o in rng G implies o in the carrier of F )
assume o in rng G ; :: thesis: o in the carrier of F
then o in P by E;
hence o in the carrier of F ; :: thesis: verum

end;

then rng G c= the carrier of F ;
then reconsider G1 = G as FinSequence of F by FINSEQ_1:def 4;
B6: Sum G = Sum G1 by I1, FIELD_4:2;
then B5: ( P is add-closed & Sum G1 in P & y1 in P ) by G6, D, IV, B10, AS;
Sum f = (Sum G) + (Sum <*y*>) by B2, RLVECT_1:41
.= (Sum G) + y by RLVECT_1:44
.= (Sum G1) + y1 by I1, B6, FIELD_6:15 ;
hence Sum f in P by B5; :: thesis: verum

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: len f = n ;
thus Sum f in P by AS, I, H; :: thesis: verum