scheme :: RECDEF_1:sch 12
LambdaDefRec{ F₁() -> object , F₂() -> Nat, F₃( object , object ) -> set } :

( ex y being set ex f being Function st
( y = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F₂() & dom f = NAT & f . 0 = F₁() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) holds
y1 = y2 ) )