scheme :: ALGSTR_4:sch 4
FuncRecursiveExist2{ F₁() -> non empty set , F₂( XFinSequence of F₁()) -> Element of F₁() } :

ex f being sequence of F₁() st
for n being Nat holds f . n = F₂((f | n))