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

F₅() = F₆()

provided

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