let fs be FinSequence of REAL ; :: thesis: for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) holds
Sum (Seq fss) <= Sum fs
let fss be Subset of fs; :: thesis: ( ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) implies Sum (Seq fss) <= Sum fs )
defpred S₁[ Nat] means for fs being FinSequence of REAL
for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = $1 holds
Sum (Seq fss) <= Sum fs;
assume A1: for i being Element of NAT st i in dom fs holds
0 <= fs . i ; :: thesis: Sum (Seq fss) <= Sum fs
A2: len (Seq fss) = len (Seq fss) ;

now :: thesis: for k being Nat st S₁[k] holds
for fs being FinSequence of REAL
for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = k + 1 holds
Sum (Seq fss) <= Sum fs

let k be Nat; :: thesis: ( S₁[k] implies for fs being FinSequence of REAL
for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = k + 1 holds
Sum (Seq fss) <= Sum fs )
assume A3: S₁[k] ; :: thesis: for fs being FinSequence of REAL
for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = k + 1 holds
Sum (Seq fss) <= Sum fs
let fs be FinSequence of REAL ; :: thesis: for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = k + 1 holds
Sum (Seq fss) <= Sum fs
let fss be Subset of fs; :: thesis: ( ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = k + 1 implies Sum (Seq fss) <= Sum fs )
assume that
A4: for i being Element of NAT st i in dom fs holds
0 <= fs . i and
A5: len (Seq fss) = k + 1 ; :: thesis: Sum (Seq fss) <= Sum fs
consider q being FinSequence of REAL , z being Element of REAL such that
A6: Seq fss = q ^ <*z*> by A5, FINSEQ_2:19;
card fss = k + 1 by A5, GLIB_001:5;
then dom fss <> {} by CARD_1:27, RELAT_1:41;
then consider d being object such that
A7: d in dom fss by XBOOLE_0:def 1;
A8: dom fss c= dom fs by FINSEQ_6:151;
then A9: d in dom fs by A7;
defpred S₂[ Nat] means $1 in dom fss;
consider L being Nat such that
A10: dom fss c= Seg L by FINSEQ_1:def 12;
A11: for n being Nat st S₂[n] holds
n <= L by A10, FINSEQ_1:1;
reconsider d = d as Element of NAT by A9;
d in dom fss by A7;
then A12: ex d being Nat st S₂[d] ;
consider x being Nat such that
A13: ( S₂[x] & ( for n being Nat st S₂[n] holds
n <= x ) ) from NAT_1:sch 6(A11, A12);
set y = fs . x;
A14: len (Seq fss) = (len q) + (len <*z*>) by A6, FINSEQ_1:22;
then A15: k + 1 = (len q) + 1 by A5, FINSEQ_1:39;

now :: thesis: fs . x = z

set g = Sgm (dom fss);
1 <= k + 1 by NAT_1:12;
then A16: len (Seq fss) in dom (Seq fss) by A5, FINSEQ_3:25;
A17: len (Seq fss) = card fss by GLIB_001:5
.= card (dom fss) by CARD_1:62
.= len (Sgm (dom fss)) by FINSEQ_3:39 ;

A18: now :: thesis: not (Sgm (dom fss)) . (len (Seq fss)) <> x

set k2 = (Sgm (dom fss)) . (len (Sgm (dom fss)));
assume A19: (Sgm (dom fss)) . (len (Seq fss)) <> x ; :: thesis: contradiction
1 <= len (Sgm (dom fss)) by A5, A17, NAT_1:12;
then len (Sgm (dom fss)) in dom (Sgm (dom fss)) by FINSEQ_3:25;
then A20: (Sgm (dom fss)) . (len (Sgm (dom fss))) in rng (Sgm (dom fss)) by FUNCT_1:def 3;
reconsider k2 = (Sgm (dom fss)) . (len (Sgm (dom fss))) as Element of NAT ;
A21: rng (Sgm (dom fss)) = dom fss by FINSEQ_1:def 14;
then consider v being object such that
A22: v in dom (Sgm (dom fss)) and
A23: (Sgm (dom fss)) . v = x by A13, FUNCT_1:def 3;
reconsider v = v as Element of NAT by A22;
v <= len (Sgm (dom fss)) by A22, FINSEQ_3:25;
then A24: v < len (Sgm (dom fss)) by A17, A19, A23, XXREAL_0:1;
1 <= v by A22, FINSEQ_3:25;
then x < k2 by A23, A24, FINSEQ_1:def 14;
hence contradiction by A13, A21, A20; :: thesis: verum

end;

( (Seq fss) . (len (Seq fss)) = z & Seq fss = fss * (Sgm (dom fss)) ) by A5, A6, A15, FINSEQ_1:42, FINSEQ_1:def 15;
then fss . ((Sgm (dom fss)) . (len (Seq fss))) = z by A16, FUNCT_1:12;
then [x,z] in fss by A13, A18, FUNCT_1:1;
hence fs . x = z by FUNCT_1:1; :: thesis: verum

end;

then A25: Sum (Seq fss) = (fs . x) + (Sum q) by A6, RVSUM_1:74;
A26: x <= len fs by A8, A13, FINSEQ_3:25;
then consider j being Nat such that
A27: x + j = len fs by NAT_1:10;
A28: 1 <= x by A8, A13, FINSEQ_3:25;
then reconsider xx1 = x - 1 as Element of NAT by INT_1:5;
set fssq = fss | (Seg xx1);
reconsider fssq = fss | (Seg xx1) as Subset of fs by FINSEQ_6:153;
consider fsD, fsC being FinSequence of REAL such that
A29: len fsD = x and
len fsC = j and
A30: fs = fsD ^ fsC by A27, FINSEQ_2:23;
A31: xx1 + 1 = x ;
then consider fsA, fsB being FinSequence of REAL such that
A32: len fsA = xx1 and
A33: len fsB = 1 and
A34: fsD = fsA ^ fsB by A29, FINSEQ_2:23;
x in dom fsD by A28, A29, FINSEQ_3:25;
then A35: fs . x = fsD . x by A30, FINSEQ_1:def 7;

now :: thesis: for z being object st z in fssq holds
z in fsA

let z be object ; :: thesis: ( z in fssq implies z in fsA )
assume A36: z in fssq ; :: thesis: z in fsA
then consider a, b being object such that
A37: z = [a,b] by RELAT_1:def 1;
A38: a in Seg xx1 by A36, A37, RELAT_1:def 11;
then reconsider a = a as Element of NAT ;
A39: a <= xx1 by A38, FINSEQ_1:1;
A40: 1 <= a by A38, FINSEQ_1:1;
then A41: a in dom fsA by A32, A39, FINSEQ_3:25;
A42: b = fs . a by A36, A37, FUNCT_1:1;
a + 0 <= x by A31, A39, XREAL_1:7;
then a in dom fsD by A29, A40, FINSEQ_3:25;
then b = fsD . a by A30, A42, FINSEQ_1:def 7;
then b = fsA . a by A34, A41, FINSEQ_1:def 7;
hence z in fsA by A37, A41, FUNCT_1:1; :: thesis: verum

end;

then reconsider fssq = fssq as Subset of fsA by TARSKI:def 3;

now :: thesis: ( len q = len (Seq fssq) & ( for n being Nat st 1 <= n & n <= len q holds
q . n = (Seq fssq) . n ) )

A43: now :: thesis: for z being object st z in {[x,(fs . x)]} holds
z in fss

let z be object ; :: thesis: ( z in {[x,(fs . x)]} implies z in fss )
assume z in {[x,(fs . x)]} ; :: thesis: z in fss
then A44: z = [x,(fs . x)] by TARSKI:def 1;
[x,(fss . x)] in fss by A13, FUNCT_1:1;
hence z in fss by A44, FUNCT_1:1; :: thesis: verum

end;

now :: thesis: for z being object holds
( ( z in fssq implies z in fss \ {[x,(fs . x)]} ) & ( z in fss \ {[x,(fs . x)]} implies z in fssq ) )

[x,(fs . x)] in {[x,(fs . x)]} by TARSKI:def 1;
then A45: [x,(fs . x)] in fss by A43;
let z be object ; :: thesis: ( ( z in fssq implies z in fss \ {[x,(fs . x)]} ) & ( z in fss \ {[x,(fs . x)]} implies z in fssq ) )

hereby :: thesis: ( z in fss \ {[x,(fs . x)]} implies z in fssq )

assume A46: z in fssq ; :: thesis: z in fss \ {[x,(fs . x)]}
then consider a, b being object such that
A47: z = [a,b] by RELAT_1:def 1;
A48: a in Seg xx1 by A46, A47, RELAT_1:def 11;
then reconsider a = a as Element of NAT ;
a <= xx1 by A48, FINSEQ_1:1;
then a < x by A31, NAT_1:13;
then [a,b] <> [x,(fs . x)] by XTUPLE_0:1;
then A49: not z in {[x,(fs . x)]} by A47, TARSKI:def 1;
z in fss by A46, A47, RELAT_1:def 11;
hence z in fss \ {[x,(fs . x)]} by A49, XBOOLE_0:def 5; :: thesis: verum

end;

assume A50: z in fss \ {[x,(fs . x)]} ; :: thesis: z in fssq
then consider a, b being object such that
A51: z = [a,b] by RELAT_1:def 1;
A52: a in dom fs by A50, A51, FUNCT_1:1;
A53: z in fss by A50, XBOOLE_0:def 5;
then A54: a in dom fss by A51, FUNCT_1:1;
reconsider a = a as Element of NAT by A52;
A55: a <= x by A13, A54;
not z in {[x,(fs . x)]} by A50, XBOOLE_0:def 5;
then ( a <> x or b <> fs . x ) by A51, TARSKI:def 1;
then a <> x by A50, A51, A45, FUNCT_1:def 1;
then a < x by A55, XXREAL_0:1;
then a + 1 <= x by NAT_1:13;
then A56: (a + 1) - 1 <= x - 1 by XREAL_1:13;
1 <= a by A52, FINSEQ_3:25;
then a in Seg xx1 by A56, FINSEQ_1:1;
hence z in fssq by A51, A53, RELAT_1:def 11; :: thesis: verum

end;

then A57: fssq = fss \ {[x,(fs . x)]} by TARSKI:2;

now :: thesis: for z being object holds
( ( z in dom fss implies z in (dom fssq) \/ {x} ) & ( z in (dom fssq) \/ {x} implies z in dom fss ) )

let z be object ; :: thesis: ( ( z in dom fss implies z in (dom fssq) \/ {x} ) & ( z in (dom fssq) \/ {x} implies z in dom fss ) )

hereby :: thesis: ( z in (dom fssq) \/ {x} implies z in dom fss )

assume A58: z in dom fss ; :: thesis: z in (dom fssq) \/ {x}
then A59: [z,(fss . z)] in fss by FUNCT_1:1;
then A60: z in dom fs by FUNCT_1:1;
then reconsider z9 = z as Element of NAT ;
A61: 1 <= z9 by A60, FINSEQ_3:25;
A62: z9 <= x by A13, A58;

now :: thesis: ( not z in {x} implies z in dom fssq )

assume not z in {x} ; :: thesis: z in dom fssq
then z <> x by TARSKI:def 1;
then z9 < xx1 + 1 by A62, XXREAL_0:1;
then z9 <= xx1 by NAT_1:13;
then z9 in Seg xx1 by A61, FINSEQ_1:1;
then [z,(fss . z)] in fssq by A59, RELAT_1:def 11;
hence z in dom fssq by FUNCT_1:1; :: thesis: verum

end;

hence z in (dom fssq) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

assume A63: z in (dom fssq) \/ {x} ; :: thesis: z in dom fss

now :: thesis: z in dom fss

per cases ( z in dom fssq or z in {x} ) by A63, XBOOLE_0:def 3;

suppose z in dom fssq ; :: thesis: z in dom fss

then [z,(fssq . z)] in fssq by FUNCT_1:1;
then [z,(fssq . z)] in fss by RELAT_1:def 11;
hence z in dom fss by FUNCT_1:1; :: thesis: verum

end;

suppose z in {x} ; :: thesis: z in dom fss

hence z in dom fss by A13, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence z in dom fss ; :: thesis: verum

end;

then A64: dom fss = (dom fssq) \/ {x} by TARSKI:2;
A65: card fss = k + 1 by A5, GLIB_001:5;

A66: now :: thesis: for m, n being Nat st m in dom fssq & n in {x} holds
m < n

let m, n be Nat; :: thesis: ( m in dom fssq & n in {x} implies m < n )
assume that
A67: m in dom fssq and
A68: n in {x} ; :: thesis: m < n
[m,(fssq . m)] in fssq by A67, FUNCT_1:1;
then m in Seg xx1 by RELAT_1:def 11;
then A69: m <= xx1 by FINSEQ_1:1;
n = x by A68, TARSKI:def 1;
hence m < n by A31, A69, NAT_1:13; :: thesis: verum

end;

{[x,(fs . x)]} c= fss by A43, TARSKI:def 3;
then A70: card fssq = (card fss) - (card {[x,(fs . x)]}) by A57, CARD_2:44
.= (k + 1) - 1 by A65, CARD_1:30
.= k ;
hence len q = len (Seq fssq) by A15, GLIB_001:5; :: thesis: for n being Nat st 1 <= n & n <= len q holds
q . n = (Seq fssq) . n
let n be Nat; :: thesis: ( 1 <= n & n <= len q implies q . n = (Seq fssq) . n )
set x1 = (Sgm (dom fss)) . n;
set x2 = (Sgm (dom fssq)) . n;
assume that
A71: 1 <= n and
A72: n <= len q ; :: thesis: q . n = (Seq fssq) . n
n in dom q by A71, A72, FINSEQ_3:25;
then A73: q . n = (Seq fss) . n by A6, FINSEQ_1:def 7;
len (Sgm (dom fssq)) = card (dom fssq) by FINSEQ_3:39
.= k by A70, CARD_1:62 ;
then A75: n in dom (Sgm (dom fssq)) by A15, A71, A72, FINSEQ_3:25;
then (Sgm (dom fssq)) . n in rng (Sgm (dom fssq)) by FUNCT_1:def 3;
then (Sgm (dom fssq)) . n in dom fssq by FINSEQ_1:def 14;
then [((Sgm (dom fssq)) . n),(fssq . ((Sgm (dom fssq)) . n))] in fssq by FUNCT_1:1;
then [((Sgm (dom fssq)) . n),(fssq . ((Sgm (dom fssq)) . n))] in fss by RELAT_1:def 11;
then A76: fss . ((Sgm (dom fssq)) . n) = fssq . ((Sgm (dom fssq)) . n) by FUNCT_1:1;
n <= k + 1 by A5, A14, A72, NAT_1:12;
then A77: n in dom (Seq fss) by A5, A71, FINSEQ_3:25;
Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 15;
then A78: q . n = fss . ((Sgm (dom fss)) . n) by A73, A77, FUNCT_1:12;
A79: Seq fssq = fssq * (Sgm (dom fssq)) by FINSEQ_1:def 15;
len (Seq fssq) = card fssq by GLIB_001:5;
then n in dom (Seq fssq) by A15, A70, A71, A72, FINSEQ_3:25;
then A80: (Seq fssq) . n = fssq . ((Sgm (dom fssq)) . n) by A79, FUNCT_1:12;

now :: thesis: for z being object st z in {x} holds
z in Seg (len fs)

let z be object ; :: thesis: ( z in {x} implies z in Seg (len fs) )
assume z in {x} ; :: thesis: z in Seg (len fs)
then z = x by TARSKI:def 1;
hence z in Seg (len fs) by A28, A26, FINSEQ_1:1; :: thesis: verum

end;

then {x} c= Seg (len fs) by TARSKI:def 3;
then {x} is included_in_Seg by FINSEQ_1:def 13;
then Sgm (dom fss) = (Sgm (dom fssq)) ^ (Sgm {x}) by A64, A66, FINSEQ_3:42;
hence q . n = (Seq fssq) . n by A78, A80, A75, A76, FINSEQ_1:def 7; :: thesis: verum

end;

then A81: q = Seq fssq by FINSEQ_1:14;

now :: thesis: for i being Element of NAT st i in dom fsA holds
0 <= fsA . i

A82: dom fsD c= dom fs by A30, FINSEQ_1:26;
let i be Element of NAT ; :: thesis: ( i in dom fsA implies 0 <= fsA . i )
A83: dom fsA c= dom fsD by A34, FINSEQ_1:26;
assume A84: i in dom fsA ; :: thesis: 0 <= fsA . i
then fsA . i = fsD . i by A34, FINSEQ_1:def 7;
then A85: fsA . i = fs . i by A30, A84, A83, FINSEQ_1:def 7;
i in dom fsD by A84, A83;
hence 0 <= fsA . i by A4, A85, A82; :: thesis: verum

end;

then Sum q <= Sum fsA by A3, A15, A81;
then (Sum (Seq fss)) + (Sum q) <= ((fs . x) + (Sum q)) + (Sum fsA) by A25, XREAL_1:7;
then (Sum (Seq fss)) + (Sum q) <= ((fs . x) + (Sum fsA)) + (Sum q) ;
then A86: Sum (Seq fss) <= (Sum fsA) + (fs . x) by XREAL_1:6;

now :: thesis: for i being Nat st i in dom fsC holds
0 <= fsC . i

let i be Nat; :: thesis: ( i in dom fsC implies 0 <= fsC . i )
assume i in dom fsC ; :: thesis: 0 <= fsC . i
then ( fs . (x + i) = fsC . i & x + i in dom fs ) by A29, A30, FINSEQ_1:28, FINSEQ_1:def 7;
hence 0 <= fsC . i by A4; :: thesis: verum

end;

then A87: 0 <= Sum fsC by RVSUM_1:84;
1 in dom fsB by A33, FINSEQ_3:25;
then fs . x = fsB . 1 by A31, A32, A34, A35, FINSEQ_1:def 7;
then A88: fsB = <*(fs . x)*> by A33, FINSEQ_1:40;
reconsider y = fs . x as Element of REAL by XREAL_0:def 1;
Sum fs = (Sum fsD) + (Sum fsC) by A30, RVSUM_1:75
.= ((Sum fsA) + (Sum <*y*>)) + (Sum fsC) by A34, A88, RVSUM_1:75
.= ((Sum fsA) + y) + (Sum fsC) by FINSOP_1:11 ;
then ((Sum fsA) + y) + 0 <= Sum fs by A87, XREAL_1:7;
hence Sum (Seq fss) <= Sum fs by A86, XXREAL_0:2; :: thesis: verum

end;

then A89: for k being Nat st S₁[k] holds
S₁[k + 1] ;

now :: thesis: for fs being FinSequence of REAL
for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = 0 holds
Sum (Seq fss) <= Sum fs

let fs be FinSequence of REAL ; :: thesis: for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = 0 holds
Sum (Seq fss) <= Sum fs
let fss be Subset of fs; :: thesis: ( ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = 0 implies Sum (Seq fss) <= Sum fs )
assume ( ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) & len (Seq fss) = 0 ) ; :: thesis: Sum (Seq fss) <= Sum fs
then ( ( for i being Nat st i in dom fs holds
0 <= fs . i ) & Seq fss = <*> REAL ) ;
hence Sum (Seq fss) <= Sum fs by RVSUM_1:72, RVSUM_1:84; :: thesis: verum

end;

then A90: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A90, A89);
hence Sum (Seq fss) <= Sum fs by A1, A2; :: thesis: verum