deffunc H₁( Element of NAT ) -> Element of REAL = Rseq . ($1,0);
consider f0 being Function of NAT,REAL such that
a0: for n being Element of NAT holds f0 . n = H₁(n) from FUNCT_2:sch 4();
deffunc H₂( real number , Nat, Nat) -> set = $1 + (Rseq . ($2,($3 + 1)));
consider IT being Function of [:NAT,NAT:],REAL such that
a1: for a being Element of NAT holds
( IT . (a,0) = f0 . a & ( for n being natural number holds IT . (a,(n + 1)) = H₂(IT . (a,n),a,n) ) ) from DBLSEQ_2:sch 2();
take IT ; :: thesis: for n, m being Nat holds
( IT . (n,0) = Rseq . (n,0) & IT . (n,(m + 1)) = (IT . (n,m)) + (Rseq . (n,(m + 1))) )

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( IT . (n,0) = Rseq . (n,0) & IT . (n,(m + 1)) = (IT . (n,m)) + (Rseq . (n,(m + 1))) )
a2: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
then IT . (n,0) = f0 . n by a1;
hence ( IT . (n,0) = Rseq . (n,0) & IT . (n,(m + 1)) = (IT . (n,m)) + (Rseq . (n,(m + 1))) ) by a0, a1, a2; :: thesis: verum

end;