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

{ F₃(F₂(),i) where i is Nat : ( i in dom F₂() & P₁[i] ) } is finite