deffunc H1( Element of NAT ) -> Element of ExtREAL = f . ($1,0);
consider f0 being Function of NAT,ExtREAL such that
A1:
for n being Element of NAT holds f0 . n = H1(n)
from FUNCT_2:sch 4();
deffunc H2( Element of ExtREAL , Nat, Nat) -> Element of ExtREAL = $1 + (f . ($2,($3 + 1)));
consider IT being Function of [:NAT,NAT:],ExtREAL such that
A2:
for a being Element of NAT holds
( IT . (a,0) = f0 . a & ( for n being Nat holds IT . (a,(n + 1)) = H2(IT . (a,n),a,n) ) )
from DBLSEQ_2:sch 1();
take
IT
; for n, m being Nat holds
( IT . (n,0) = f . (n,0) & IT . (n,(m + 1)) = (IT . (n,m)) + (f . (n,(m + 1))) )
hereby verum
let n,
m be
Nat;
( IT . (n,0) = f . (n,0) & IT . (n,(m + 1)) = (IT . (n,m)) + (f . (n,(m + 1))) )A3:
(
n in NAT &
m in NAT )
by ORDINAL1:def 12;
then
IT . (
n,
0)
= f0 . n
by A2;
hence
(
IT . (
n,
0)
= f . (
n,
0) &
IT . (
n,
(m + 1))
= (IT . (n,m)) + (f . (n,(m + 1))) )
by A1, A2, A3;
verum
end;