let a be non empty FinSequence of REAL ; :: thesis: ex nf 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 nf . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf . (s,f) = (f . (len f)) + 1 ) )

defpred S_{1}[ object , object , object ] means ex s being Real ex f being FinSequence of NAT st

( $1 = s & $2 = f & ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies $3 = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies $3 = (f . (len f)) + 1 ) );

A1: for s, f being object st s in REAL & f in NAT * holds

ex z being object st

( z in NAT & S_{1}[s,f,z] )

L100: for s, f being object st s in REAL & f in NAT * holds

S_{1}[s,f,nf . (s,f)]
from BINOP_1:sch 1(A1);

take nf ; :: thesis: for s being Real

for f being FinSequence of NAT holds

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

thus for s being Real

for f being FinSequence of NAT holds

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

for s being Real

for f being FinSequence of NAT holds

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

defpred S

( $1 = s & $2 = f & ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies $3 = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies $3 = (f . (len f)) + 1 ) );

A1: for s, f being object st s in REAL & f in NAT * holds

ex z being object st

( z in NAT & S

proof

consider nf being Function of [:REAL,(NAT *):],NAT such that
let s, f be object ; :: thesis: ( s in REAL & f in NAT * implies ex z being object st

( z in NAT & S_{1}[s,f,z] ) )

assume that

L030: s in REAL and

L031: f in NAT * ; :: thesis: ex z being object st

( z in NAT & S_{1}[s,f,z] )

reconsider s0 = s as Real by L030;

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

end;( z in NAT & S

assume that

L030: s in REAL and

L031: f in NAT * ; :: thesis: ex z being object st

( z in NAT & S

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 )
;

end;

suppose L050:
s0 + (SumBin (a,f0,{(f0 . (len f0))})) <= 1
; :: thesis: ex z being object st

( z in NAT & S_{1}[s,f,z] )

( z in NAT & S

take z = f0 . (len f0); :: thesis: ( z in NAT & S_{1}[s,f,z] )

thus z in NAT by ORDINAL1:def 12; :: thesis: S_{1}[s,f,z]

thus S_{1}[s,f,z]
by L050; :: thesis: verum

end;thus z in NAT by ORDINAL1:def 12; :: thesis: S

thus S

suppose L060:
s0 + (SumBin (a,f0,{(f0 . (len f0))})) > 1
; :: thesis: ex z being object st

( z in NAT & S_{1}[s,f,z] )

( z in NAT & S

take z = (f0 . (len f0)) + 1; :: thesis: ( z in NAT & S_{1}[s,f,z] )

thus z in NAT by ORDINAL1:def 12; :: thesis: S_{1}[s,f,z]

thus S_{1}[s,f,z]
by L060; :: thesis: verum

end;thus z in NAT by ORDINAL1:def 12; :: thesis: S

thus S

L100: for s, f being object st s in REAL & f in NAT * holds

S

take nf ; :: thesis: for s being Real

for f being FinSequence of NAT holds

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

thus for s being Real

for f being FinSequence of NAT holds

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

proof

let s be Real; :: thesis: for f being FinSequence of NAT holds

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

let f be FinSequence of NAT ; :: thesis: ( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf . (s,f) = (f . (len f)) + 1 ) )

f in NAT * by FINSEQ_1:def 11;

then consider s0 being Real, f0 being FinSequence of NAT such that

L350: ( s = s0 & f = f0 & ( s0 + (SumBin (a,f0,{(f0 . (len f0))})) <= 1 implies nf . (s,f) = f0 . (len f0) ) & ( s0 + (SumBin (a,f0,{(f0 . (len f0))})) > 1 implies nf . (s,f) = (f0 . (len f0)) + 1 ) ) by XREAL_0:def 1, L100;

thus ( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf . (s,f) = (f . (len f)) + 1 ) ) by L350; :: thesis: verum

end;( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf . (s,f) = (f . (len f)) + 1 ) )

let f be FinSequence of NAT ; :: thesis: ( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf . (s,f) = (f . (len f)) + 1 ) )

f in NAT * by FINSEQ_1:def 11;

then consider s0 being Real, f0 being FinSequence of NAT such that

L350: ( s = s0 & f = f0 & ( s0 + (SumBin (a,f0,{(f0 . (len f0))})) <= 1 implies nf . (s,f) = f0 . (len f0) ) & ( s0 + (SumBin (a,f0,{(f0 . (len f0))})) > 1 implies nf . (s,f) = (f0 . (len f0)) + 1 ) ) by XREAL_0:def 1, L100;

thus ( ( s + (SumBin (a,f,{(f . (len f))})) <= 1 implies nf . (s,f) = f . (len f) ) & ( s + (SumBin (a,f,{(f . (len f))})) > 1 implies nf . (s,f) = (f . (len f)) + 1 ) ) by L350; :: thesis: verum