scheme :: RECDEF_2:sch 10
LambdaRec3Un{ F₁() -> object , F₂() -> object , F₃() -> object , F₄() -> Function, F₅() -> Function, F₆( object , object , object , object ) -> object } :

F₄() = F₅()

provided

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