scheme :: NAT_1:sch 3
DefbyInd{ F₁() -> Nat, F₂( Nat, Nat) -> Nat, P₁[ Nat, Nat] } :

( ( for k being Nat ex n being Nat st P₁[k,n] ) & ( for k, n, m being Nat st P₁[k,n] & P₁[k,m] holds
n = m ) )

provided

A1: for k, n being Nat holds
( P₁[k,n] iff ( ( k = 0 & n = F₁() ) or ex m, l being Nat st
( k = m + 1 & P₁[m,l] & n = F₂(k,l) ) ) )