let F1, F2 be Function of [:NAT,NAT:],REAL; ( ( for m, n being Nat holds F1 . (m,n) = 1 / (m + 1) ) & ( for m, n being Nat holds F2 . (m,n) = 1 / (m + 1) ) implies F1 = F2 )
assume that
A1:
for m, n being Nat holds F1 . (m,n) = 1 / (m + 1)
and
A2:
for m, n being Nat holds F2 . (m,n) = 1 / (m + 1)
; F1 = F2
hence
F1 = F2
by FUNCT_1:def 11; verum