let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT
for k being Nat
for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ) holds
Sum R1 = SumBin (a,f,(rng f))
let f be FinSequence of NAT ; :: thesis: for k being Nat
for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ) holds
Sum R1 = SumBin (a,f,(rng f))
let k be Nat; :: thesis: for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ) holds
Sum R1 = SumBin (a,f,(rng f))
let R1 be real-valued FinSequence; :: thesis: ( dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ) implies Sum R1 = SumBin (a,f,(rng f)) )
assume that
L00: dom f = dom a and
L30: rng f = Seg k and
L40: len R1 = k and
L41: for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ; :: thesis: Sum R1 = SumBin (a,f,(rng f))
A00: dom R1 = Seg k by L40, FINSEQ_1:def 3;
rng f <> {} by L00, RELAT_1:42;
then 0 < k by L30;
then A94: 0 + 1 <= k by INT_1:7;
defpred S₁[ Nat] means for r1segi being real-valued FinSequence st r1segi = R1 | (Seg $1) holds
Sum r1segi = SumBin (a,f,(Seg $1));
reconsider k = k as Element of NAT by ORDINAL1:def 12;
for r1segi being real-valued FinSequence st r1segi = R1 | (Seg 1) holds
Sum r1segi = SumBin (a,f,(Seg 1))

proof

let r1seg1 be real-valued FinSequence; :: thesis: ( r1seg1 = R1 | (Seg 1) implies Sum r1seg1 = SumBin (a,f,(Seg 1)) )
assume A10: r1seg1 = R1 | (Seg 1) ; :: thesis: Sum r1seg1 = SumBin (a,f,(Seg 1))
then A18: dom r1seg1 = Seg 1 by A94, L40, FINSEQ_1:17;
A19: 1 in dom R1 by A00, A94;
1 in Seg 1 ;
then A20: r1seg1 . 1 = R1 . 1 by A10, FUNCT_1:49
.= SumBin (a,f,(Seg 1)) by A19, L41, FINSEQ_1:2 ;
r1seg1 = <*(SumBin (a,f,(Seg 1)))*> by A18, A20, FINSEQ_1:def 8;
hence Sum r1seg1 = SumBin (a,f,(Seg 1)) by RVSUM_1:73; :: thesis: verum

end;

then A30: S₁[1] ;
A60: for i being Element of NAT st 1 <= i & i < k & S₁[i] holds
S₁[i + 1]

proof

let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < k & S₁[i0] implies S₁[i0 + 1] )
assume that
1 <= i0 and
A62: i0 < k and
A63: S₁[i0] ; :: thesis: S₁[i0 + 1]
reconsider r1segi0 = R1 | (Seg i0) as real-valued FinSequence by FINSEQ_1:15;
reconsider r1segi0p = R1 | (Seg (i0 + 1)) as real-valued FinSequence by FINSEQ_1:15;
A733: 1 <= i0 + 1 by NAT_1:12;
i0 + 1 <= k by A62, INT_1:7;
then A74: i0 + 1 in dom R1 by A733, A00;
then A80: Sum r1segi0p = Sum (r1segi0 ^ <*(R1 . (i0 + 1))*>) by FINSEQ_5:10
.= (Sum r1segi0) + (R1 . (i0 + 1)) by RVSUM_1:74
.= (Sum r1segi0) + (SumBin (a,f,{(i0 + 1)})) by A74, L41 ;
SumBin (a,f,(Seg (i0 + 1))) = SumBin (a,f,((Seg i0) \/ {(i0 + 1)})) by FINSEQ_1:9
.= (SumBin (a,f,(Seg i0))) + (SumBin (a,f,{(i0 + 1)})) by FINSEQ_3:14, NF270
.= Sum r1segi0p by A63, A80 ;
hence for r1segi being real-valued FinSequence st r1segi = R1 | (Seg (i0 + 1)) holds
Sum r1segi = SumBin (a,f,(Seg (i0 + 1))) ; :: thesis: verum

end;

A89: for i being Element of NAT st 1 <= i & i <= k holds
S₁[i] from INT_1:sch 7(A30, A60);
R1 = R1 | (dom R1)
.= R1 | (Seg k) by L40, FINSEQ_1:def 3 ;
hence Sum R1 = SumBin (a,f,(rng f)) by L30, A94, A89; :: thesis: verum