let F1, F2 be Function of [:NAT,NAT:],REAL; :: thesis: ( ( 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) ; :: thesis: 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) ; :: thesis: F1 = F2

now :: thesis: ( dom F1 = dom F2 & ( for x being object st x in dom F1 holds

F1 . x = F2 . x ) )

hence
F1 = F2
by FUNCT_1:def 11; :: thesis: verumF1 . x = F2 . x ) )

( dom F1 = [:NAT,NAT:] & dom F2 = [:NAT,NAT:] )
by FUNCT_2:def 1;

hence dom F1 = dom F2 ; :: thesis: for x being object st x in dom F1 holds

F1 . x = F2 . x

end;hence dom F1 = dom F2 ; :: thesis: for x being object st x in dom F1 holds

F1 . x = F2 . x

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )

assume x in dom F1 ; :: thesis: F1 . x = F2 . x

then consider n1, n2 being object such that

A4: n1 in NAT and

A5: n2 in NAT and

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

reconsider n1 = n1, n2 = n2 as Nat by A4, A5;

thus F1 . x = F1 . (n1,n2) by A6, BINOP_1:def 1

.= 1 / (n1 + 1) by A1

.= F2 . (n1,n2) by A2

.= F2 . x by A6, BINOP_1:def 1 ; :: thesis: verum

end;assume x in dom F1 ; :: thesis: F1 . x = F2 . x

then consider n1, n2 being object such that

A4: n1 in NAT and

A5: n2 in NAT and

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

reconsider n1 = n1, n2 = n2 as Nat by A4, A5;

thus F1 . x = F1 . (n1,n2) by A6, BINOP_1:def 1

.= 1 / (n1 + 1) by A1

.= F2 . (n1,n2) by A2

.= F2 . x by A6, BINOP_1:def 1 ; :: thesis: verum