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