scheme :: SPPOL_1:sch 2
FinSeqFam9{ F₁() -> non empty set , F₂() -> FinSequence of F₁(), F₃( FinSequence of F₁(), Nat) -> set , P₁[ set ] } :

{ F₃(F₂(),i) where i is Nat : ( 1 <= i & i <= len F₂() & P₁[i] ) } is finite