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
now :: thesis: ( dom F1 = dom F2 & ( for x being object st x in dom F1 holds
F1 . 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
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;
end;
hence F1 = F2 by FUNCT_1:def 11; :: thesis: verum