scheme :: ALGSTR_4:sch 4
FuncRecursiveExist2{ F1() -> non empty set , F2( XFinSequence of F1()) -> Element of F1() } :
ex f being sequence of F1() st
for n being Nat holds f . n = F2((f | n))