scheme :: RECDEF_2:sch 6
LambdaRec2Un{ F₁() -> object , F₂() -> object , F₃() -> Function, F₄() -> Function, F₅( object , object , object ) -> object } :

F₃() = F₄()

provided

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