let a be non empty at_most_one FinSequence of REAL ; :: thesis: 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; :: thesis: ( j in rng (idseq (len a)) implies SumBin (a,(idseq (len a)),{j}) <= 1 )
assume L5910: j in rng (idseq (len a)) ; :: thesis: 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; :: thesis: verum

end;

L592: rng (idseq (len a)) = Seg (len a) ;
take len a ; :: thesis: 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) )

proof

reconsider f1 = idseq (len a) as non empty FinSequence of NAT by L592, FINSEQ_1:def 4;
take f1 ; :: thesis: ( dom f1 = dom a & ( for j being Nat st j in rng f1 holds
SumBin (a,f1,{j}) <= 1 ) & len a = card (rng f1) )
thus ( dom f1 = dom a & ( for j being Nat st j in rng f1 holds
SumBin (a,f1,{j}) <= 1 ) & len a = card (rng f1) ) by FINSEQ_1:def 3, L591, FINSEQ_1:57; :: thesis: verum

end;

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) ) ; :: thesis: verum