scheme :: RECDEF_1:sch 14
LambdaDefRecD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, F₄( object , object ) -> Element of F₁() } :

( ex y being Element of F₁() ex f being sequence of F₁() st
( y = f . F₃() & f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₄(n,(f . n)) ) ) & ( for y1, y2 being Element of F₁() st ex f being sequence of F₁() st
( y1 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₄(n,(f . n)) ) ) & ex f being sequence of F₁() st
( y2 = f . F₃() & f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₄(n,(f . n)) ) ) holds
y1 = y2 ) )