defpred S1[ 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 holds
ex y being object st
( y in REAL & S1[x,y] )
proof
let x be object ; :: thesis: ( x in implies ex y being object st
( y in REAL & S1[x,y] ) )

assume x in ; :: thesis: ex y being object st
( y in REAL & S1[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 & S1[x,y] )
thus y in REAL by XREAL_0:def 1; :: thesis: S1[x,y]
thus S1[x,y] by A3, A4; :: thesis: verum
end;
consider f being Function of ,REAL such that
A5: for x being object st x in holds
S1[x,f . x] from
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 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
.= 1 / (m + 1) by ;
hence f . (m,n) = 1 / (m + 1) ; :: thesis: verum
end;
hence ex b1 being Function of ,REAL st
for m, n being Nat holds b1 . (m,n) = 1 / (m + 1) ; :: thesis: verum