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₁( 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₁(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

proof

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;

then L55: R1 is FinSequence of REAL by NF315;
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

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;

then L80: Sum R1 <= Sum R2 by RVSUM_1:82;
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