let a be non empty at_most_one FinSequence of REAL ; :: thesis: for opt1, opt2 being Element of NAT st 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 ) & opt1 = 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
opt1 <= card (rng f) ) ) & 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 ) & opt2 = 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
opt2 <= card (rng f) ) ) holds
opt1 = opt2
let opt1, opt2 be Element of NAT ; :: 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 ) & opt1 = 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
opt1 <= card (rng f) ) ) & 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 ) & opt2 = 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
opt2 <= card (rng f) ) ) implies opt1 = opt2 )
assume that
L000: 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 ) & opt1 = 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
opt1 <= card (rng f) ) ) and
L001: 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 ) & opt2 = 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
opt2 <= card (rng f) ) ) ; :: thesis: opt1 = opt2
consider g1 being non empty FinSequence of NAT such that
L010: dom g1 = dom a and
L011: for j being Nat st j in rng g1 holds
SumBin (a,g1,{j}) <= 1 and
L012: opt1 = card (rng g1) and
L013: 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
opt1 <= card (rng f) by L000;
consider g2 being non empty FinSequence of NAT such that
L020: dom g2 = dom a and
L021: for j being Nat st j in rng g2 holds
SumBin (a,g2,{j}) <= 1 and
L022: opt2 = card (rng g2) and
L023: 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
opt2 <= card (rng f) by L001;
L050: opt1 <= opt2 by L020, L021, L013, L022;
opt2 <= opt1 by L010, L011, L023, L012;
hence opt1 = opt2 by L050, XXREAL_0:1; :: thesis: verum