let f1, f2 be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ( for n, m being Nat holds
( f1 . (n,0) = f . (n,0) & f1 . (n,(m + 1)) = (f1 . (n,m)) + (f . (n,(m + 1))) ) ) & ( for n, m being Nat holds
( f2 . (n,0) = f . (n,0) & f2 . (n,(m + 1)) = (f2 . (n,m)) + (f . (n,(m + 1))) ) ) implies f1 = f2 )
assume that
A1: for n, m being natural number holds
( f1 . (n,0) = f . (n,0) & f1 . (n,(m + 1)) = (f1 . (n,m)) + (f . (n,(m + 1))) ) and
A2: for n, m being natural number holds
( f2 . (n,0) = f . (n,0) & f2 . (n,(m + 1)) = (f2 . (n,m)) + (f . (n,(m + 1))) ) ; :: thesis: f1 = f2
A3: ( dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] ) by FUNCT_2:def 1;
for n, m being object st n in NAT & m in NAT holds
f1 . (n,m) = f2 . (n,m)

proof

let n, m be object ; :: thesis: ( n in NAT & m in NAT implies f1 . (n,m) = f2 . (n,m) )
assume ( n in NAT & m in NAT ) ; :: thesis: f1 . (n,m) = f2 . (n,m)
then reconsider n1 = n, m1 = m as Element of NAT ;
defpred S₁[ Nat] means f1 . (n1,$1) = f2 . (n1,$1);
f1 . (n1,0) = f . (n1,0) by A1;
then A4: S₁[ 0 ] by A2;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
f1 . (n1,(k + 1)) = (f1 . (n1,k)) + (f . (n1,(k + 1))) by A1;
hence f1 . (n1,(k + 1)) = f2 . (n1,(k + 1)) by A2, A6; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
then S₁[m1] ;
hence f1 . (n,m) = f2 . (n,m) ; :: thesis: verum

end;

hence f1 = f2 by A3, FUNCT_3:6; :: thesis: verum