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

F₄() = F₅()

provided

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