ex q being V43() sequence of NAT st
( ( for n being Nat holds P₁[(F₁() * 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 n = q . m ) )

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