scheme :: STIRL2_1:sch 1
Sch1{ F₁() -> Nat, F₂() -> Nat, P₁[ set ] } :

{ f where f is Function of (Segm F₁()),(Segm F₂()) : P₁[f] } is finite