let a be non empty FinSequence of REAL ; :: thesis: for Alg being Function of [:REAL,(NAT *):],NAT holds (OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg))) is non empty FinSequence of NAT
let Alg be Function of [:REAL,(NAT *):],NAT; :: thesis: (OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg))) is non empty FinSequence of NAT
set h = OnlinePackingHistory (a,Alg);
L150: 1 <= len (OnlinePackingHistory (a,Alg)) by NAT_1:14;
L170: len (OnlinePackingHistory (a,Alg)) = len a by defPackHistory;
then len ((OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg)))) = len (OnlinePackingHistory (a,Alg)) by L150, NF510;
hence (OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg))) is non empty FinSequence of NAT by L150, L170, NF505; :: thesis: verum