let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,(NextFit a)) holds

for i, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds

(h . i) . i = k

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies for i, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds

(h . i) . i = k )

assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds

(h . i) . i = k

let i, k be Nat; :: thesis: ( 1 <= i & i <= len a & rng (h . i) = Seg k implies (h . i) . i = k )

assume that

L410: 1 <= i and

L415: i <= len a and

L417: rng (h . i) = Seg k ; :: thesis: (h . i) . i = k

consider k0 being Nat such that

L427: rng (h . i) = Seg k0 and

L428: (h . i) . i = k0 by HN00, L410, L415, NF805;

thus (h . i) . i = k by L417, L427, FINSEQ_1:6, L428; :: thesis: verum

for i, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds

(h . i) . i = k

let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies for i, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds

(h . i) . i = k )

assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds

(h . i) . i = k

let i, k be Nat; :: thesis: ( 1 <= i & i <= len a & rng (h . i) = Seg k implies (h . i) . i = k )

assume that

L410: 1 <= i and

L415: i <= len a and

L417: rng (h . i) = Seg k ; :: thesis: (h . i) . i = k

consider k0 being Nat such that

L427: rng (h . i) = Seg k0 and

L428: (h . i) . i = k0 by HN00, L410, L415, NF805;

thus (h . i) . i = k by L417, L427, FINSEQ_1:6, L428; :: thesis: verum