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