defpred S₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in [:NAT,NAT:] implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in [:NAT,NAT:] ; :: thesis: ex y being object st
( y in REAL & S₁[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₁[x,y] )
thus y in REAL by XREAL_0:def 1; :: thesis: S₁[x,y]
thus S₁[x,y] by A3, A4; :: thesis: verum

end;

consider f being Function of [:NAT,NAT:],REAL such that
A5: for x being object st x in [:NAT,NAT:] holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);

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

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

hence ex b₁ being Function of [:NAT,NAT:],REAL st
for m, n being Nat holds b₁ . (m,n) = 1 / (m + 1) ; :: thesis: verum