scheme :: FRAENKEL:sch 27
FuncsChoice{ F₁() -> non empty set , F₂() -> non empty set , P₁[ Element of F₁(), Element of F₂()], F₃() -> Element of Fin F₁() } :

ex ff being Element of Funcs (F₁(),F₂()) st
for t being Element of F₁() st t in F₃() holds
P₁[t,ff . t]

provided

A1: for t being Element of F₁() st t in F₃() holds
ex ff being Element of F₂() st P₁[t,ff]