defpred S_{1}[ object , object ] means ex r being Real ex n1, n2 being Nat st

( $1 = [n1,n2] & $2 = r & r = 1 / (n1 + 1) );

A1: for x being object st x in [:NAT,NAT:] holds

ex y being object st

( y in REAL & S_{1}[x,y] )

A5: for x being object st x in [:NAT,NAT:] holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A1);

_{1} being Function of [:NAT,NAT:],REAL st

for m, n being Nat holds b_{1} . (m,n) = 1 / (m + 1)
; :: thesis: verum

( $1 = [n1,n2] & $2 = r & r = 1 / (n1 + 1) );

A1: for x being object st x in [:NAT,NAT:] holds

ex y being object st

( y in REAL & S

proof

consider f being Function of [:NAT,NAT:],REAL such that
let x be object ; :: thesis: ( x in [:NAT,NAT:] implies ex y being object st

( y in REAL & S_{1}[x,y] ) )

assume x in [:NAT,NAT:] ; :: thesis: ex y being object st

( y in REAL & S_{1}[x,y] )

then consider n1, n2 being object such that

A2: n1 in NAT and

A3: n2 in NAT and

A4: x = [n1,n2] by ZFMISC_1:def 2;

reconsider n1 = n1, n2 = n2 as Nat by A2, A3;

reconsider y = 1 / (n1 + 1) as Real ;

take y ; :: thesis: ( y in REAL & S_{1}[x,y] )

thus y in REAL by XREAL_0:def 1; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A3, A4; :: thesis: verum

end;( y in REAL & S

assume x in [:NAT,NAT:] ; :: thesis: ex y being object st

( y in REAL & S

then consider n1, n2 being object such that

A2: n1 in NAT and

A3: n2 in NAT and

A4: x = [n1,n2] by ZFMISC_1:def 2;

reconsider n1 = n1, n2 = n2 as Nat by A2, A3;

reconsider y = 1 / (n1 + 1) as Real ;

take y ; :: thesis: ( y in REAL & S

thus y in REAL by XREAL_0:def 1; :: thesis: S

thus S

A5: for x being object st x in [:NAT,NAT:] holds

S

now :: thesis: for m, n being Nat holds f . (m,n) = 1 / (m + 1)

hence
ex blet m, n be Nat; :: thesis: f . (m,n) = 1 / (m + 1)

( m in NAT & n in NAT ) by ORDINAL1:def 12;

then [m,n] in [:NAT,NAT:] by ZFMISC_1:def 2;

then consider r being Real, n1, n2 being Nat such that

A6: [m,n] = [n1,n2] and

A7: f . [m,n] = r and

A8: r = 1 / (n1 + 1) by A5;

f . (m,n) = r by A7, BINOP_1:def 1

.= 1 / (m + 1) by A8, A6, XTUPLE_0:1 ;

hence f . (m,n) = 1 / (m + 1) ; :: thesis: verum

end;( m in NAT & n in NAT ) by ORDINAL1:def 12;

then [m,n] in [:NAT,NAT:] by ZFMISC_1:def 2;

then consider r being Real, n1, n2 being Nat such that

A6: [m,n] = [n1,n2] and

A7: f . [m,n] = r and

A8: r = 1 / (n1 + 1) by A5;

f . (m,n) = r by A7, BINOP_1:def 1

.= 1 / (m + 1) by A8, A6, XTUPLE_0:1 ;

hence f . (m,n) = 1 / (m + 1) ; :: thesis: verum

for m, n being Nat holds b