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

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) )

( 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

( 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

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

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

hence
ex f being non empty FinSequence of NAT st
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;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

( 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