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 & rng (h . (i + 1)) = Seg (k + 1) holds
(SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1
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 & rng (h . (i + 1)) = Seg (k + 1) holds
(SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1 )
assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i, k being Nat st 1 <= i & i < len a & rng (h . i) = Seg k & rng (h . (i + 1)) = Seg (k + 1) holds
(SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1
let i, k be Nat; :: thesis: ( 1 <= i & i < len a & rng (h . i) = Seg k & rng (h . (i + 1)) = Seg (k + 1) implies (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1 )
assume that
L060: 1 <= i and
L061: i < len a and
L062: rng (h . i) = Seg k and
L063: rng (h . (i + 1)) = Seg (k + 1) ; :: thesis: (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1
reconsider hi = h . i as FinSequence of NAT by HN00, L060, L061, NF505;
L030: hi <> {} by HN00, L060, L061, NF510;

L013: now :: thesis: 1 <= k

assume not 1 <= k ; :: thesis: contradiction
then k < 0 + 1 ;
then k <= 0 by NAT_1:13;
hence contradiction by L062, L030; :: thesis: verum

end;

reconsider ip = i + 1 as Element of NAT by ORDINAL1:def 12;
L074: 1 + 0 <= i + 1 by XREAL_1:7;
L076: ip <= len a by L061, NAT_1:13;
reconsider hip = h . ip as FinSequence of NAT by HN00, L074, L076, NF505;
L080: hip = hi ^ <*((NextFit a) . ((a . ip),hi))*> by HN00, L060, L061, NF520;
L081: hip . ip = (NextFit a) . ((a . ip),hi) by HN00, L060, L061, NF520;
L100: ( ( (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) <= 1 implies (NextFit a) . ((a . ip),hi) = hi . (len hi) ) & ( (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) > 1 implies (NextFit a) . ((a . ip),hi) = (hi . (len hi)) + 1 ) ) by defNextFit;

L499: now :: thesis: (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) > 1

assume not (a . ip) + (SumBin (a,hi,{(hi . (len hi))})) > 1 ; :: thesis: contradiction
then L140: hip . ip = hi . (len hi) by L081, defNextFit
.= hi . i by HN00, L060, L061, NF510
.= k by HN00, L060, L061, L062, NF807 ;
L149: k in Seg k by L013;
rng (h . (i + 1)) = (rng (h . i)) \/ {k} by HN00, L060, L061, NF525, L140
.= Seg k by L062, L149, ZFMISC_1:31, XBOOLE_1:12 ;
then k = k + 1 by L063, FINSEQ_1:6;
hence contradiction ; :: thesis: verum

end;

reconsider kp = k + 1 as Nat ;
len (h . ip) = ip by HN00, L074, L076, NF510;
then L540: (h . ip) . (len (h . ip)) = k + 1 by HN00, L074, L076, L063, NF807;
L559: len (hi ^ <*((hi . (len hi)) + 1)*>) = (len hi) + (len <*((hi . (len hi)) + 1)*>) by FINSEQ_1:22
.= (len hi) + 1 by FINSEQ_1:40 ;
L599: (h . ip) . (len (h . ip)) = (hi . (len hi)) + 1 by FINSEQ_1:42, L100, L499, L080, L559;
L649: len hi = ip - 1 by HN00, L060, L061, NF510;
L670: (len hi) + 1 <= len a by HN00, L060, L061, NF510, L076;
k + 1 <> k ;
then L700: SumBin (a,(h . ip),{k}) = SumBin (a,hi,{(hi . (len hi))}) by L100, L499, L080, L599, L540, NF110;
L799: SumBin (a,(hi ^ <*(k + 1)*>),{(k + 1)}) = (SumBin (a,hi,{(k + 1)})) + (a . ((len hi) + 1)) by L670, NF200;
0 <= SumBin (a,hi,{(k + 1)}) by NF280;
then ((a . ip) + (SumBin (a,hi,{(hi . (len hi))}))) + 0 <= ((a . ip) + (SumBin (a,hi,{(hi . (len hi))}))) + (SumBin (a,hi,{(k + 1)})) by XREAL_1:7;
hence (SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1 by L499, L700, L799, L599, L540, L100, L080, L649, XXREAL_0:2; :: thesis: verum