let f1, f2 be Function of [:NAT,NAT:],REAL; :: thesis: ( ( 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)) ) ; :: 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 . ($1,m1) = f2 . ($1,m1);
f1 . (0,m1) = Rseq . (0,m1) 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 . ((k + 1),m1) = (f1 . (k,m1)) + (Rseq . ((k + 1),m1)) by a1;
hence f1 . ((k + 1),m1) = f2 . ((k + 1),m1) by a2, a6; :: thesis: verum

end;

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

end;

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