deffunc H1( Element of NAT ) -> Element of REAL = Rseq . (0,$1);
consider f0 being Function of NAT,REAL such that
a0:
for n being Element of NAT holds f0 . n = H1(n)
from FUNCT_2:sch 4();
deffunc H2( Real, Nat, Nat) -> set = $1 + (Rseq . (($3 + 1),$2));
consider IT being Function of [:NAT,NAT:],REAL such that
a1:
for a being Element of NAT holds
( IT . (0,a) = f0 . a & ( for n being natural number holds IT . ((n + 1),a) = H2(IT . (n,a),a,n) ) )
from DBLSEQ_2:sch 4();
take
IT
; for n, m being Nat holds
( IT . (0,m) = Rseq . (0,m) & IT . ((n + 1),m) = (IT . (n,m)) + (Rseq . ((n + 1),m)) )
hereby verum
let n,
m be
natural number ;
( IT . (0,m) = Rseq . (0,m) & IT . ((n + 1),m) = (IT . (n,m)) + (Rseq . ((n + 1),m)) )a2:
(
n in NAT &
m in NAT )
by ORDINAL1:def 12;
then
IT . (
0,
m)
= f0 . m
by a1;
hence
(
IT . (
0,
m)
= Rseq . (
0,
m) &
IT . (
(n + 1),
m)
= (IT . (n,m)) + (Rseq . ((n + 1),m)) )
by a0, a1, a2;
verum
end;