scheme :: ALGSTR_4:sch 2
FuncRecursiveExist{ F₁( set ) -> set } :

ex f being Function st
( dom f = NAT & ( for n being Nat holds f . n = F₁((f | n)) ) )