deffunc H₁( Element of NAT ) -> Element of ExtREAL = f . (0,$1);
consider f0 being Function of NAT,ExtREAL such that
A1: for n being Element of NAT holds f0 . n = H₁(n) from FUNCT_2:sch 4();
deffunc H₂( Element of ExtREAL , Nat, Nat) -> Element of ExtREAL = $1 + (f . (($3 + 1),$2));
consider IT being Function of [:NAT,NAT:],ExtREAL such that
A2: for a being Element of NAT holds
( IT . (0,a) = f0 . a & ( for n being Nat holds IT . ((n + 1),a) = H₂(IT . (n,a),a,n) ) ) from DBLSEQ_2:sch 3();
take IT ; :: thesis: for n, m being Nat holds
( IT . (0,m) = f . (0,m) & IT . ((n + 1),m) = (IT . (n,m)) + (f . ((n + 1),m)) )

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( IT . (0,m) = f . (0,m) & IT . ((n + 1),m) = (IT . (n,m)) + (f . ((n + 1),m)) )
A3: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
then IT . (0,m) = f0 . m by A2;
hence ( IT . (0,m) = f . (0,m) & IT . ((n + 1),m) = (IT . (n,m)) + (f . ((n + 1),m)) ) by A1, A2, A3; :: thesis: verum

end;