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
len (h . i) = i
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
len (h . i) = i
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
len (h . i) = i )
assume L00: h = OnlinePackingHistory (a,Alg) ; :: thesis: for i being Nat st 1 <= i & i <= len a holds
len (h . i) = i
defpred S₁[ Nat] means len (h . $1) = $1;
h . 1 = <*1*> by L00, defPackHistory;
then L05: S₁[1] by FINSEQ_1:39;
L08: for i being Element of NAT st 1 <= i & i < len a & S₁[i] holds
S₁[i + 1]

proof

let im be Element of NAT ; :: thesis: ( 1 <= im & im < len a & S₁[im] implies S₁[im + 1] )
assume that
L10: ( 1 <= im & im < len a ) and
L15: len (h . im) = im ; :: thesis: S₁[im + 1]
consider d1 being Element of REAL , d2 being FinSequence of NAT such that
L20: ( d1 = a . (im + 1) & d2 = h . im ) and
L30: h . (im + 1) = d2 ^ <*(Alg . (d1,d2))*> by L00, L10, defPackHistory;
len (h . (im + 1)) = (len (h . im)) + (len <*(Alg . ((a . (im + 1)),(h . im)))*>) by L20, L30, FINSEQ_1:22
.= im + 1 by FINSEQ_1:39, L15 ;
hence S₁[im + 1] ; :: thesis: verum

end;

L800: for i being Element of NAT st 1 <= i & i <= len a holds
S₁[i] from INT_1:sch 7(L05, L08);
for i being Nat st 1 <= i & i <= len a holds
S₁[i]

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len a implies S₁[i] )
assume that
L810: 1 <= i and
L811: i <= len a ; :: thesis: S₁[i]
i in NAT by ORDINAL1:def 12;
hence S₁[i] by L810, L811, L800; :: thesis: verum

end;

hence for i being Nat st 1 <= i & i <= len a holds
len (h . i) = i ; :: thesis: verum