scheme :: HILB10_5:sch 1
SCH1{ P₁[ object , object ], F₁() -> XFinSequence-yielding XFinSequence } :

{ ((F₁() . i) . j) where i, j is Nat : P₁[i,j] } is finite