scheme :: NAT_1:sch 15
LambdaRecUn{ F₁() -> object , F₂( object , object ) -> object , F₃() -> Function, F₄() -> Function } :

F₃() = F₄()

provided

A1: dom F₃() = NAT and
A2: F₃() . 0 = F₁() and
A3: for n being Nat holds F₃() . (n + 1) = F₂(n,(F₃() . n)) and
A4: dom F₄() = NAT and
A5: F₄() . 0 = F₁() and
A6: for n being Nat holds F₄() . (n + 1) = F₂(n,(F₄() . n))