let a be non empty at_most_one FinSequence of REAL ; :: thesis: [/(Sum a)\] <= Opt a
consider g1 being non empty FinSequence of NAT such that
L00: dom g1 = dom a and
L10: for j being Nat st j in rng g1 holds
SumBin (a,g1,{j}) <= 1 and
L20: Opt a = card (rng g1) and
for 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 ) holds
Opt a <= card (rng f) by defOpt;
thus [/(Sum a)\] <= Opt a by L00, L10, NF320, L20; :: thesis: verum