let a be non empty positive FinSequence of REAL ; :: thesis: for Alg being Function of [:REAL,(NAT *):],NAT
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds
for i, l being Nat st 1 <= i & i < len a holds
SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})
let Alg be Function of [:REAL,(NAT *):],NAT; :: thesis: for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds
for i, l being Nat st 1 <= i & i < len a holds
SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})
let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,Alg) implies for i, l being Nat st 1 <= i & i < len a holds
SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l}) )
assume HC00: h = OnlinePackingHistory (a,Alg) ; :: thesis: for i, l being Nat st 1 <= i & i < len a holds
SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})
let i, l be Nat; :: thesis: ( 1 <= i & i < len a implies SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l}) )
assume that
L000: 1 <= i and
L001: i < len a ; :: thesis: SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})
L120: h . i is FinSequence of NAT by HC00, L000, L001, NF505;
L147: i + 1 <= len a by L001, NAT_1:13;
then L150: (len (h . i)) + 1 <= len a by HC00, L000, L001, NF510;
i + 1 in dom a by L147, XREAL_1:38, FINSEQ_3:25;
then a . (i + 1) in rng a by FUNCT_1:3;
then reconsider aip = a . (i + 1) as Element of REAL ;
reconsider hi = h . i as Element of NAT * by L120, FINSEQ_1:def 11;
L190: Alg . (aip,hi) is Nat ;

per cases ( Alg . ((a . (i + 1)),(h . i)) = l or Alg . ((a . (i + 1)),(h . i)) <> l ) ;

suppose L200: Alg . ((a . (i + 1)),(h . i)) = l ; :: thesis: SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})

L279: SumBin (a,(h . (i + 1)),{l}) = SumBin (a,((h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*>),{l}) by HC00, L000, L001, NF520
.= (SumBin (a,(h . i),{l})) + (a . ((len (h . i)) + 1)) by L120, L150, L200, NF200 ;
(len (h . i)) + 1 in dom a by XREAL_1:38, L150, FINSEQ_3:25;
hence SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l}) by L279, RVSUM_3:def 1, XREAL_1:29; :: thesis: verum

end;

suppose L500: Alg . ((a . (i + 1)),(h . i)) <> l ; :: thesis: SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})

reconsider b = Alg . ((a . (i + 1)),(h . i)) as Nat by L190;
SumBin (a,(h . (i + 1)),{l}) = SumBin (a,((h . i) ^ <*b*>),{l}) by HC00, L000, L001, NF520
.= SumBin (a,(h . i),{l}) by L120, L500, NF110 ;
hence SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l}) ; :: thesis: verum

end;

end;