scheme :: VALUED_1:sch 1
SubSeqChoice{ F1() -> non empty set , F2() -> sequence of F1(), P1[ set ] } :
ex S1 being subsequence of F2() st
for n being Element of NAT holds P1[S1 . n]
provided
A1: for n being Element of NAT ex m being Element of NAT st
( n <= m & P1[F2() . m] )