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