scheme :: DBLSEQ_2:sch 3
RecEx2D2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Function of F₁(),F₂(), F₄( set , set , Nat) -> Element of F₂() } :

ex g being Function of [:NAT,F₁():],F₂() st
for a being Element of F₁() holds
( g . (0,a) = F₃() . a & ( for n being Nat holds g . ((n + 1),a) = F₄((g . (n,a)),a,n) ) )