let a be non empty 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 being Nat st 1 <= i & i <= len a holds

h . i is FinSequence of NAT

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 being Nat st 1 <= i & i <= len a holds

h . i is FinSequence of NAT

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,Alg) implies for i being Nat st 1 <= i & i <= len a holds

h . i is FinSequence of NAT )

assume HC00: h = OnlinePackingHistory (a,Alg) ; :: thesis: for i being Nat st 1 <= i & i <= len a holds

h . i is FinSequence of NAT

let i be Nat; :: thesis: ( 1 <= i & i <= len a implies h . i is FinSequence of NAT )

assume that

L000: 1 <= i and

L001: i <= len a ; :: thesis: h . i is FinSequence of NAT

L023: i <= len h by HC00, defPackHistory, L001;

reconsider i = i as Element of dom h by L000, L023, FINSEQ_3:25;

h . i is FinSequence of NAT ;

hence h . i is FinSequence of NAT ; :: thesis: verum

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 is FinSequence of NAT

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 being Nat st 1 <= i & i <= len a holds

h . i is FinSequence of NAT

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,Alg) implies for i being Nat st 1 <= i & i <= len a holds

h . i is FinSequence of NAT )

assume HC00: h = OnlinePackingHistory (a,Alg) ; :: thesis: for i being Nat st 1 <= i & i <= len a holds

h . i is FinSequence of NAT

let i be Nat; :: thesis: ( 1 <= i & i <= len a implies h . i is FinSequence of NAT )

assume that

L000: 1 <= i and

L001: i <= len a ; :: thesis: h . i is FinSequence of NAT

L023: i <= len h by HC00, defPackHistory, L001;

reconsider i = i as Element of dom h by L000, L023, FINSEQ_3:25;

h . i is FinSequence of NAT ;

hence h . i is FinSequence of NAT ; :: thesis: verum