let f1, f2 be Function of [:NAT,NAT:],REAL; ( ( for n, m being Nat holds
( f1 . (0,m) = Rseq . (0,m) & f1 . ((n + 1),m) = (f1 . (n,m)) + (Rseq . ((n + 1),m)) ) ) & ( for n, m being Nat holds
( f2 . (0,m) = Rseq . (0,m) & f2 . ((n + 1),m) = (f2 . (n,m)) + (Rseq . ((n + 1),m)) ) ) implies f1 = f2 )
assume that
a1:
for n, m being natural number holds
( f1 . (0,m) = Rseq . (0,m) & f1 . ((n + 1),m) = (f1 . (n,m)) + (Rseq . ((n + 1),m)) )
and
a2:
for n, m being natural number holds
( f2 . (0,m) = Rseq . (0,m) & f2 . ((n + 1),m) = (f2 . (n,m)) + (Rseq . ((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)
= Rseq . (
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)) + (Rseq . ((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