scheme :: NAT_1:sch 16
LambdaRecUnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( object , object ) -> Element of F₁(), F₄() -> sequence of F₁(), F₅() -> sequence of F₁() } :

F₄() = F₅()

provided

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