let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1 ) holds

[/(Sum a)\] <= card (rng f)

let f be FinSequence of NAT ; :: thesis: ( dom f = dom a & ( for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1 ) implies [/(Sum a)\] <= card (rng f) )

assume that

L00: dom f = dom a and

L10: for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1 ; :: thesis: [/(Sum a)\] <= card (rng f)

consider fr being FinSequence of NAT such that

L25: dom fr = dom a and

L26: for j being Nat st j in rng fr holds

SumBin (a,fr,{j}) <= 1 and

L27: ex k being Nat st rng fr = Seg k and

L28: card (rng f) = card (rng fr) by L00, L10, NF305;

consider i being Nat such that

L29: rng fr = Seg i by L27;

deffunc H_{1}( Nat) -> Real = SumBin (a,fr,{$1});

ex p being FinSequence st

( len p = i & ( for j being Nat st j in dom p holds

p . j = H_{1}(j) ) )
from FINSEQ_1:sch 2();

then consider R1 being FinSequence such that

L40: len R1 = i and

L41: for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,fr,{j}) ;

for j being Nat st j in dom R1 holds

R1 . j in REAL

R1 is i -element by L40;

then reconsider R1 = R1 as i -element real-valued FinSequence by L55;

reconsider R2 = i |-> 1 as i -element real-valued FinSequence ;

for j being Nat st j in Seg i holds

R1 . j <= R2 . j

L90: Sum R1 = SumBin (a,fr,(rng fr)) by L25, L29, L40, L41, NF310;

Sum R2 = i * 1 by RVSUM_1:80

.= card (rng f) by L29, FINSEQ_1:57, L28 ;

then Sum a <= card (rng f) by L80, L90, L25, NF260;

hence [/(Sum a)\] <= card (rng f) by INT_1:65; :: thesis: verum

SumBin (a,f,{j}) <= 1 ) holds

[/(Sum a)\] <= card (rng f)

let f be FinSequence of NAT ; :: thesis: ( dom f = dom a & ( for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1 ) implies [/(Sum a)\] <= card (rng f) )

assume that

L00: dom f = dom a and

L10: for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1 ; :: thesis: [/(Sum a)\] <= card (rng f)

consider fr being FinSequence of NAT such that

L25: dom fr = dom a and

L26: for j being Nat st j in rng fr holds

SumBin (a,fr,{j}) <= 1 and

L27: ex k being Nat st rng fr = Seg k and

L28: card (rng f) = card (rng fr) by L00, L10, NF305;

consider i being Nat such that

L29: rng fr = Seg i by L27;

deffunc H

ex p being FinSequence st

( len p = i & ( for j being Nat st j in dom p holds

p . j = H

then consider R1 being FinSequence such that

L40: len R1 = i and

L41: for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,fr,{j}) ;

for j being Nat st j in dom R1 holds

R1 . j in REAL

proof

then L55:
R1 is FinSequence of REAL
by NF315;
let j be Nat; :: thesis: ( j in dom R1 implies R1 . j in REAL )

assume j in dom R1 ; :: thesis: R1 . j in REAL

then R1 . j = SumBin (a,fr,{j}) by L41;

hence R1 . j in REAL by XREAL_0:def 1; :: thesis: verum

end;assume j in dom R1 ; :: thesis: R1 . j in REAL

then R1 . j = SumBin (a,fr,{j}) by L41;

hence R1 . j in REAL by XREAL_0:def 1; :: thesis: verum

R1 is i -element by L40;

then reconsider R1 = R1 as i -element real-valued FinSequence by L55;

reconsider R2 = i |-> 1 as i -element real-valued FinSequence ;

for j being Nat st j in Seg i holds

R1 . j <= R2 . j

proof

then L80:
Sum R1 <= Sum R2
by RVSUM_1:82;
let j be Nat; :: thesis: ( j in Seg i implies R1 . j <= R2 . j )

assume L71: j in Seg i ; :: thesis: R1 . j <= R2 . j

Seg i = dom R1 by L40, FINSEQ_1:def 3;

then L78: R1 . j = SumBin (a,fr,{j}) by L71, L41;

R2 . j = 1 by L71, FINSEQ_2:57;

hence R1 . j <= R2 . j by L78, L26, L29, L71; :: thesis: verum

end;assume L71: j in Seg i ; :: thesis: R1 . j <= R2 . j

Seg i = dom R1 by L40, FINSEQ_1:def 3;

then L78: R1 . j = SumBin (a,fr,{j}) by L71, L41;

R2 . j = 1 by L71, FINSEQ_2:57;

hence R1 . j <= R2 . j by L78, L26, L29, L71; :: thesis: verum

L90: Sum R1 = SumBin (a,fr,(rng fr)) by L25, L29, L40, L41, NF310;

Sum R2 = i * 1 by RVSUM_1:80

.= card (rng f) by L29, FINSEQ_1:57, L28 ;

then Sum a <= card (rng f) by L80, L90, L25, NF260;

hence [/(Sum a)\] <= card (rng f) by INT_1:65; :: thesis: verum