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
rng (h . (i + 1)) = (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))}
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
rng (h . (i + 1)) = (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))}
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
rng (h . (i + 1)) = (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))} )
assume L00: h = OnlinePackingHistory (a,Alg) ; :: thesis: for i being Nat st 1 <= i & i < len a holds
rng (h . (i + 1)) = (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))}
let i be Nat; :: thesis: ( 1 <= i & i < len a implies rng (h . (i + 1)) = (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))} )
assume ( 1 <= i & i < len a ) ; :: thesis: rng (h . (i + 1)) = (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))}
then ( h . (i + 1) = (h . i) ^ <*(Alg . ((a . (i + 1)),(h . i)))*> & (h . (i + 1)) . (i + 1) = Alg . ((a . (i + 1)),(h . i)) ) by L00, NF520;
hence rng (h . (i + 1)) = (rng (h . i)) \/ (rng <*((h . (i + 1)) . (i + 1))*>) by FINSEQ_1:31
.= (rng (h . i)) \/ {((h . (i + 1)) . (i + 1))} by FINSEQ_1:38 ;
:: thesis: verum