scheme :: RECDEF_2:sch 11
LambdaRec3UnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> sequence of F₁(), F₆() -> sequence of F₁(), F₇( object , object , object , object ) -> Element of F₁() } :

F₅() = F₆()

provided

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