scheme :: ORDINAL2:sch 20
LambdaRecUn{ F₁() -> set , F₂( set , set ) -> set , F₃() -> Function, F₄() -> Function } :

F₃() = F₄()

provided

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