let a be non empty FinSequence of REAL ; :: thesis: for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,(NextFit a)) holds
for i being Nat st 1 <= i & i <= len a holds
ex k being Nat st
( rng (h . i) = Seg k & (h . i) . i = k )
let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies for i being Nat st 1 <= i & i <= len a holds
ex k being Nat st
( rng (h . i) = Seg k & (h . i) . i = k ) )
assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i being Nat st 1 <= i & i <= len a holds
ex k being Nat st
( rng (h . i) = Seg k & (h . i) . i = k )
defpred S₁[ Nat] means ex k being Nat st
( rng (h . $1) = Seg k & (h . $1) . $1 = k );
(OnlinePackingHistory (a,(NextFit a))) . 1 = {[1,1]} by defPackHistory;
then L219: rng (h . 1) = {1} by HN00, RELAT_1:9;
L289: h . 1 = <*1*> by defPackHistory, HN00;
L300: S₁[1] by L219, FINSEQ_1:2, L289;
L400: for i being Element of NAT st 1 <= i & i < len a & S₁[i] holds
S₁[i + 1]

proof

let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < len a & S₁[i0] implies S₁[i0 + 1] )
assume that
L410: 1 <= i0 and
L411: i0 < len a and
L412: S₁[i0] ; :: thesis: S₁[i0 + 1]
reconsider hi0 = h . i0 as FinSequence of NAT by HN00, L410, L411, NF505;
reconsider i0p = i0 + 1 as Element of NAT by ORDINAL1:def 12;
L074: 1 + 0 <= i0 + 1 by XREAL_1:7;
L076: i0p <= len a by L411, NAT_1:13;
reconsider hi0p = h . i0p as FinSequence of NAT by HN00, L074, L076, NF505;
consider k0 being Nat such that
L427: rng hi0 = Seg k0 and
L428: (h . i0) . i0 = k0 by L412;
L090: len (h . i0) = i0 by HN00, L410, L411, NF510;
L100: ( ( (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1 implies (NextFit a) . ((a . i0p),hi0) = hi0 . i0 ) & ( (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1 implies (NextFit a) . ((a . i0p),hi0) = (hi0 . i0) + 1 ) ) by L090, defNextFit;
ex k being Nat st
( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

proof

per cases ( (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1 or (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1 ) ;

suppose L500: (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) > 1 ; :: thesis: ex k being Nat st
( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

rng hi0p = (Seg k0) \/ {(hi0p . i0p)} by HN00, L410, L411, NF525, L427;
then rng hi0p = (Seg k0) \/ {(k0 + 1)} by HN00, L410, L411, NF520, L100, L500, L428
.= Seg (k0 + 1) by FINSEQ_1:9 ;
hence ex k being Nat st
( rng (h . i0p) = Seg k & (h . i0p) . i0p = k ) by HN00, L410, L411, NF520, L100, L500, L428; :: thesis: verum

end;

suppose L700: (a . i0p) + (SumBin (a,hi0,{(hi0 . i0)})) <= 1 ; :: thesis: ex k being Nat st
( rng (h . i0p) = Seg k & (h . i0p) . i0p = k )

now :: thesis: 1 <= k0

assume not 1 <= k0 ; :: thesis: contradiction
then k0 < 0 + 1 ;
then k0 <= 0 by NAT_1:13;
then hi0 = {} by L427;
hence contradiction by HN00, L410, L411, NF510; :: thesis: verum

end;

then L739: k0 in Seg k0 ;
rng hi0p = (rng hi0) \/ {(hi0p . i0p)} by HN00, L410, L411, NF525
.= (Seg k0) \/ {k0} by L427, HN00, L410, L411, NF520, L100, L700, L428
.= Seg k0 by L739, ZFMISC_1:31, XBOOLE_1:12 ;
hence ex k being Nat st
( rng (h . i0p) = Seg k & (h . i0p) . i0p = k ) by HN00, L410, L411, NF520, L100, L700, L428; :: thesis: verum

end;

end;

end;

hence S₁[i0 + 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(L300, L400);
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
ex k being Nat st
( rng (h . i) = Seg k & (h . i) . i = k ) ; :: thesis: verum