let a be non empty FinSequence of REAL ; :: thesis: for nf1, nf2 being Function of [:REAL,(NAT *):],NAT st ( for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf1 . (s,f) = (f . (len f)) + 1 ) ) ) & ( for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf2 . (s,f) = (f . (len f)) + 1 ) ) ) holds

nf1 = nf2

let nf1, nf2 be Function of [:REAL,(NAT *):],NAT; :: thesis: ( ( for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf1 . (s,f) = (f . (len f)) + 1 ) ) ) & ( for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf2 . (s,f) = (f . (len f)) + 1 ) ) ) implies nf1 = nf2 )

assume that

L000: for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf1 . (s,f) = (f . (len f)) + 1 ) ) and

L001: for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf2 . (s,f) = (f . (len f)) + 1 ) ) ; :: thesis: nf1 = nf2

for s, f being set st s in REAL & f in NAT * holds

nf1 . (s,f) = nf2 . (s,f)

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf1 . (s,f) = (f . (len f)) + 1 ) ) ) & ( for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf2 . (s,f) = (f . (len f)) + 1 ) ) ) holds

nf1 = nf2

let nf1, nf2 be Function of [:REAL,(NAT *):],NAT; :: thesis: ( ( for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf1 . (s,f) = (f . (len f)) + 1 ) ) ) & ( for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf2 . (s,f) = (f . (len f)) + 1 ) ) ) implies nf1 = nf2 )

assume that

L000: for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf1 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf1 . (s,f) = (f . (len f)) + 1 ) ) and

L001: for s being Real

for f being FinSequence of NAT holds

( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf2 . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf2 . (s,f) = (f . (len f)) + 1 ) ) ; :: thesis: nf1 = nf2

for s, f being set st s in REAL & f in NAT * holds

nf1 . (s,f) = nf2 . (s,f)

proof

hence
nf1 = nf2
; :: thesis: verum
let s, f be set ; :: thesis: ( s in REAL & f in NAT * implies nf1 . (s,f) = nf2 . (s,f) )

assume that

L030: s in REAL and

L031: f in NAT * ; :: thesis: nf1 . (s,f) = nf2 . (s,f)

reconsider s0 = s as Real by L030;

reconsider f0 = f as FinSequence of NAT by L031, FINSEQ_1:def 11;

end;assume that

L030: s in REAL and

L031: f in NAT * ; :: thesis: nf1 . (s,f) = nf2 . (s,f)

reconsider s0 = s as Real by L030;

reconsider f0 = f as FinSequence of NAT by L031, FINSEQ_1:def 11;