scheme :: STIRL2_1:sch 1
Sch1{ F1() -> Nat, F2() -> Nat, P1[ set ] } :
{ f where f is Function of (Segm F1()),(Segm F2()) : P1[f] } is finite