ex q being Real_Sequence st
( q is subsequence of F₁() & ( for n being Nat holds P₁[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F₁() . n holds
P₁[r] ) holds
ex m being Element of NAT st F₁() . n = q . m ) )

A1: for n being Element of NAT ex m being Element of NAT st
( n <= m & P₁[F₁() . m] )