theorem NF520: :: BINPACK1:23

for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds
for i being Nat st 1 <= i & i < len a holds
( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) )