scheme :: NAT_1:sch 9
CompInd1{ F1() -> Nat, P1[ Nat] } :
for k being Nat st k >= F1() holds
P1[k]
provided
A1: for k being Nat st k >= F1() & ( for n being Nat st n >= F1() & n < k holds
P1[n] ) holds
P1[k]