scheme :: AFINSQ_1:sch 4
SepXSeq{ F1() -> non empty set , P1[ XFinSequence] } :
ex X being set st
for x being object holds
( x in X iff ex p being XFinSequence st
( p in F1() ^omega & P1[p] & x = p ) )