scheme :: DBLSEQ_2:sch 2
RecEx2D1R{ F₁() -> non empty set , F₂() -> Function of F₁(),REAL, F₃( set , set , Nat) -> real number } :

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