for a being non empty FinSequence of REAL
for Alg being Function of [:REAL,(NAT *):],NAT holds (OnlinePackingHistory (a,Alg)) . 1 = {[1,1]} by defPackHistory;