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, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds
SumBin (a,(h . i),{j}) <= 1
let h be non empty FinSequence of NAT * ; :: thesis: ( h = OnlinePackingHistory (a,(NextFit a)) implies for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds
SumBin (a,(h . i),{j}) <= 1 )
assume HN00: h = OnlinePackingHistory (a,(NextFit a)) ; :: thesis: for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds
SumBin (a,(h . i),{j}) <= 1
defpred S₁[ Nat] means for j being Nat st j in rng (h . $1) holds
SumBin (a,(h . $1),{j}) <= 1;
for j being Nat st j in rng (h . 1) holds
SumBin (a,(h . 1),{j}) <= 1

proof

let j be Nat; :: thesis: ( j in rng (h . 1) implies SumBin (a,(h . 1),{j}) <= 1 )
assume FF000: j in rng (h . 1) ; :: thesis: SumBin (a,(h . 1),{j}) <= 1
FF005: 1 <= len a by NAT_1:14;
h . 1 = {[1,1]} by HN00, defPackHistory;
then rng (h . 1) = {1} by RELAT_1:9;
then FF020: j = 1 by FF000, TARSKI:def 1;
h . 1 = <*1*> by HN00, defPackHistory;
then (h . 1) . 1 = 1 ;
hence SumBin (a,(h . 1),{j}) <= 1 by FF005, HN00, NF880, FF020; :: thesis: verum

end;

then F1: S₁[1] ;
F2: for i0 being Element of NAT st 1 <= i0 & i0 < len a & S₁[i0] holds
S₁[i0 + 1]

proof

let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < len a & S₁[i0] implies S₁[i0 + 1] )
assume that
F21: ( 1 <= i0 & i0 < len a ) and
F22: S₁[i0] ; :: thesis: S₁[i0 + 1]
set i0p = i0 + 1;
F26: i0 + 1 <= len a by F21, INT_1:7;
for j being Nat st j in rng (h . (i0 + 1)) holds
SumBin (a,(h . (i0 + 1)),{j}) <= 1

proof

let j be Nat; :: thesis: ( j in rng (h . (i0 + 1)) implies SumBin (a,(h . (i0 + 1)),{j}) <= 1 )
assume I00: j in rng (h . (i0 + 1)) ; :: thesis: SumBin (a,(h . (i0 + 1)),{j}) <= 1
rng (h . (i0 + 1)) = (rng (h . i0)) \/ {((h . (i0 + 1)) . (i0 + 1))} by HN00, F21, NF525;
then rng (h . (i0 + 1)) = ((rng (h . i0)) \ {((h . (i0 + 1)) . (i0 + 1))}) \/ {((h . (i0 + 1)) . (i0 + 1))} by XBOOLE_1:39;

per cases then ( j in (rng (h . i0)) \ {((h . (i0 + 1)) . (i0 + 1))} or j in {((h . (i0 + 1)) . (i0 + 1))} ) by I00, XBOOLE_0:def 3;

suppose IA00: j in (rng (h . i0)) \ {((h . (i0 + 1)) . (i0 + 1))} ; :: thesis: SumBin (a,(h . (i0 + 1)),{j}) <= 1

IA05: j <> (h . (i0 + 1)) . (i0 + 1) by IA00, ZFMISC_1:56;
IA09: ( h . (i0 + 1) = (h . i0) ^ <*((NextFit a) . ((a . (i0 + 1)),(h . i0)))*> & (h . (i0 + 1)) . (i0 + 1) = (NextFit a) . ((a . (i0 + 1)),(h . i0)) ) by HN00, F21, NF520;
set f = h . i0;
IA35: h . i0 is FinSequence of NAT by HN00, F21, NF505;
IA36: h . (i0 + 1) is FinSequence of NAT by HN00, XREAL_1:31, F26, NF505;
set b = (h . (i0 + 1)) . (i0 + 1);
SumBin (a,(h . (i0 + 1)),{j}) = SumBin (a,(h . i0),{j}) by IA09, IA05, IA35, IA36, NF110;
hence SumBin (a,(h . (i0 + 1)),{j}) <= 1 by IA00, F22; :: thesis: verum

end;

suppose j in {((h . (i0 + 1)) . (i0 + 1))} ; :: thesis: SumBin (a,(h . (i0 + 1)),{j}) <= 1

then j = (h . (i0 + 1)) . (i0 + 1) by TARSKI:def 1;
hence SumBin (a,(h . (i0 + 1)),{j}) <= 1 by HN00, XREAL_1:31, F26, NF880; :: thesis: verum

end;

end;

end;

hence S₁[i0 + 1] ; :: thesis: verum

end;

L900: for i being Element of NAT st 1 <= i & i <= len a holds
S₁[i] from INT_1:sch 7(F1, F2);
thus for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds
SumBin (a,(h . i),{j}) <= 1 :: thesis: verum

proof

let i, j be Nat; :: thesis: ( 1 <= i & i <= len a & j in rng (h . i) implies SumBin (a,(h . i),{j}) <= 1 )
assume that
L910: ( 1 <= i & i <= len a ) and
L912: j in rng (h . i) ; :: thesis: SumBin (a,(h . i),{j}) <= 1
i in NAT by ORDINAL1:def 12;
hence SumBin (a,(h . i),{j}) <= 1 by L910, L900, L912; :: thesis: verum

end;