scheme :: HILB10_5:sch 1
SCH1{ P1[ object , object ], F1() -> XFinSequence-yielding XFinSequence } :
{ ((F1() . i) . j) where i, j is Nat : P1[i,j] } is finite