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

ex g being Function of [:NAT,F₁():],REAL 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) ) )