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)

proof

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;

per cases ( s0 + (SumBin (a,f0,{(f0 . (len f0))})) <= 1 or s0 + (SumBin (a,f0,{(f0 . (len f0))})) > 1 ) ;

suppose L050: s0 + (SumBin (a,f0,{(f0 . (len f0))})) <= 1 ; :: thesis: nf1 . (s,f) = nf2 . (s,f)

hence nf1 . (s,f) = f0 . (len f0) by L000
.= nf2 . (s,f) by L001, L050 ;
:: thesis: verum

end;

suppose L060: s0 + (SumBin (a,f0,{(f0 . (len f0))})) > 1 ; :: thesis: nf1 . (s,f) = nf2 . (s,f)

hence nf1 . (s,f) = (f0 . (len f0)) + 1 by L000
.= nf2 . (s,f) by L001, L060 ;
:: thesis: verum

end;

end;

end;

hence nf1 = nf2 ; :: thesis: verum