scheme :: FINSEQ_1:sch 4
SepSeq{ F₁() -> non empty set , P₁[ FinSequence] } :

ex X being set st
for x being object holds
( x in X iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) )