let a be non empty at_most_one FinSequence of REAL ; ex k being Nat ex f being non empty FinSequence of NAT st
( dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) & k = card (rng f) )
set k1 = len a;
set f1 = idseq (len a);
L591:
for j being Nat st j in rng (idseq (len a)) holds
SumBin (a,(idseq (len a)),{j}) <= 1
proof
let j be
Nat;
( j in rng (idseq (len a)) implies SumBin (a,(idseq (len a)),{j}) <= 1 )
assume L5910:
j in rng (idseq (len a))
;
SumBin (a,(idseq (len a)),{j}) <= 1
then L59115:
{j} c= Seg (len a)
by ZFMISC_1:31;
then L5913:
(idseq (len a)) " {j} = {j}
by FUNCT_2:94;
then
(idseq (len a)) " {j} c= dom a
by L59115, FINSEQ_1:def 3;
then L5918:
a | ((idseq (len a)) " {j}) = {[j,(a . j)]}
by L5913, ZFMISC_1:31, GRFUNC_1:28;
dom {[j,(a . j)]} = {j}
by RELAT_1:9;
then
{[j,(a . j)]} is
FinSubsequence-like
by L5910, ZFMISC_1:31;
then reconsider jaj =
{[j,(a . j)]} as
FinSubsequence ;
Seq (
a,
((idseq (len a)) " {j})) =
Seq jaj
by L5918
.=
<*(a . j)*>
by FINSEQ_3:157
;
then L5919:
SumBin (
a,
(idseq (len a)),
{j})
= a . j
by RVSUM_1:73;
L59192:
( 1
<= j &
j <= len a )
by L5910, FINSEQ_1:1;
a is
at_most_one
;
hence
SumBin (
a,
(idseq (len a)),
{j})
<= 1
by L5919, L59192;
verum
end;
L592:
rng (idseq (len a)) = Seg (len a)
;
take
len a
; ex f being non empty FinSequence of NAT st
( dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) & len a = card (rng f) )
ex f being non empty FinSequence of NAT st
( dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) & len a = card (rng f) )
hence
ex f being non empty FinSequence of NAT st
( dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) & len a = card (rng f) )
; verum