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 *
for f being non empty FinSequence of NAT holds dom (OnlinePacking (a,Alg)) = dom a
let Alg be Function of [:REAL,(NAT *):],NAT; :: thesis: for h being non empty FinSequence of NAT *
for f being non empty FinSequence of NAT holds dom (OnlinePacking (a,Alg)) = dom a
let h be non empty FinSequence of NAT * ; :: thesis: for f being non empty FinSequence of NAT holds dom (OnlinePacking (a,Alg)) = dom a
let f be non empty FinSequence of NAT ; :: thesis: dom (OnlinePacking (a,Alg)) = dom a
set f = OnlinePacking (a,Alg);
set h = OnlinePackingHistory (a,Alg);
L220: len (OnlinePackingHistory (a,Alg)) = len a by defPackHistory;
1 <= len (OnlinePackingHistory (a,Alg)) by NAT_1:14;
then len ((OnlinePackingHistory (a,Alg)) . (len (OnlinePackingHistory (a,Alg)))) = len (OnlinePackingHistory (a,Alg)) by L220, NF510;
hence dom (OnlinePacking (a,Alg)) = dom a by L220, FINSEQ_3:29; :: thesis: verum