scheme :: DBLSEQ_2:sch 1
RecEx2D1{ 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 [:F₁(),NAT:],F₂() st
for a being Element of F₁() holds
( g . (a,0) = F₃() . a & ( for n being Nat holds g . (a,(n + 1)) = F₄((g . (a,n)),a,n) ) )