scheme :: NAT_D:sch 2
INDI{ F1() -> Element of NAT , F2() -> Element of NAT , P1[ set ] } :
P1[F2()]
provided
A1: P1[ 0 ] and
A2: F1() > 0 and
A3: for i, j being Nat st P1[F1() * i] & j <> 0 & j <= F1() holds
P1[(F1() * i) + j]