let f1, f2 be Function of [:NAT,NAT:],ExtREAL; ( ( for n, m being Nat holds
( f1 . (0,m) = f . (0,m) & f1 . ((n + 1),m) = (f1 . (n,m)) + (f . ((n + 1),m)) ) ) & ( for n, m being Nat holds
( f2 . (0,m) = f . (0,m) & f2 . ((n + 1),m) = (f2 . (n,m)) + (f . ((n + 1),m)) ) ) implies f1 = f2 )
assume that
A1:
for n, m being natural number holds
( f1 . (0,m) = f . (0,m) & f1 . ((n + 1),m) = (f1 . (n,m)) + (f . ((n + 1),m)) )
and
A2:
for n, m being natural number holds
( f2 . (0,m) = f . (0,m) & f2 . ((n + 1),m) = (f2 . (n,m)) + (f . ((n + 1),m)) )
; 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 ;
( n in NAT & m in NAT implies f1 . (n,m) = f2 . (n,m) )
assume
(
n in NAT &
m in NAT )
;
f1 . (n,m) = f2 . (n,m)
then reconsider n1 =
n,
m1 =
m as
Element of
NAT ;
defpred S1[
Nat]
means f1 . ($1,
m1)
= f2 . ($1,
m1);
f1 . (
0,
m1)
= f . (
0,
m1)
by A1;
then A4:
S1[
0 ]
by A2;
A5:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
f1 . (
(k + 1),
m1)
= (f1 . (k,m1)) + (f . ((k + 1),m1))
by A1;
hence
f1 . (
(k + 1),
m1)
= f2 . (
(k + 1),
m1)
by A2, A6;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A4, A5);
then
S1[
n1]
;
hence
f1 . (
n,
m)
= f2 . (
n,
m)
;
verum
end;
hence
f1 = f2
by A3, FUNCT_3:6; verum