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₁[ 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₁[s,f,z] )

proof

let s, f be object ; :: thesis: ( s in REAL & f in NAT * implies ex z being object st
( z in NAT & S₁[s,f,z] ) )
assume that
L030: s in REAL and
L031: f in NAT * ; :: thesis: ex z being object st
( z in NAT & S₁[s,f,z] )
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: ex z being object st
( z in NAT & S₁[s,f,z] )

take z = f0 . (len f0); :: thesis: ( z in NAT & S₁[s,f,z] )
thus z in NAT by ORDINAL1:def 12; :: thesis: S₁[s,f,z]
thus S₁[s,f,z] by L050; :: thesis: verum

end;

suppose L060: s0 + (SumBin (a,f0,{(f0 . (len f0))})) > 1 ; :: thesis: ex z being object st
( z in NAT & S₁[s,f,z] )

take z = (f0 . (len f0)) + 1; :: thesis: ( z in NAT & S₁[s,f,z] )
thus z in NAT by ORDINAL1:def 12; :: thesis: S₁[s,f,z]
thus S₁[s,f,z] by L060; :: thesis: verum

end;

end;

end;

consider nf being Function of [:REAL,(NAT *):],NAT such that
L100: for s, f being object st s in REAL & f in NAT * holds
S₁[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

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;