scheme :: COMPLFLD:sch 1
Regrwithout0{ P₁[ Nat] } :

P₁[1]

provided

A1: ex k being non zero Element of NAT st P₁[k] and
A2: for k being non zero Element of NAT st k <> 1 & P₁[k] holds
ex n being non zero Element of NAT st
( n < k & P₁[n] )