let a be non empty at_most_one FinSequence of REAL ; :: thesis: ex opt being Element of NAT ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & opt = card (rng g) & ( 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 <= card (rng f) ) )
defpred S₁[ Nat] means 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 ) & $1 = card (rng f) );
L50: ex k being Nat st S₁[k] by NF300;
consider k1 being Nat such that
L60: S₁[k1] and
L62: for n being Nat st S₁[n] holds
k1 <= n from NAT_1:sch 5(L50);
consider optP being non empty FinSequence of NAT such that
L70: dom optP = dom a and
L71: for j being Nat st j in rng optP holds
SumBin (a,optP,{j}) <= 1 and
L74: k1 = card (rng optP) by L60;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
take k1 ; :: thesis: ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & k1 = card (rng g) & ( 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
k1 <= card (rng f) ) )
take optP ; :: thesis: ( dom optP = dom a & ( for j being Nat st j in rng optP holds
SumBin (a,optP,{j}) <= 1 ) & k1 = card (rng optP) & ( 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
k1 <= card (rng f) ) )
thus ( dom optP = dom a & ( for j being Nat st j in rng optP holds
SumBin (a,optP,{j}) <= 1 ) & k1 = card (rng optP) & ( 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
k1 <= card (rng f) ) ) by L70, L71, L74, L62; :: thesis: verum