scheme :: DBLSEQ_2:sch 4
RecEx2D2R{ F1() -> non empty set , F2() -> Function of F1(),REAL, F3( set , set , Nat) -> real number } :
ex g being Function of [:NAT,F1():],REAL st
for a being Element of F1() holds
( g . (0,a) = F2() . a & ( for n being Nat holds g . ((n + 1),a) = F3((g . (n,a)),a,n) ) )