scheme :: RECDEF_1:sch 8
FinRecUnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, F₄() -> FinSequence of F₁(), F₅() -> FinSequence of F₁(), P₁[ object , object , object ] } :

F₄() = F₅()

provided

A1: for n being Nat st 1 <= n & n < F₃() holds
for x, y1, y2 being Element of F₁() st P₁[n,x,y1] & P₁[n,x,y2] holds
y1 = y2 and
A2: ( len F₄() = F₃() & ( F₄() . 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,F₄() . n,F₄() . (n + 1)] ) ) and
A3: ( len F₅() = F₃() & ( F₅() . 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,F₅() . n,F₅() . (n + 1)] ) )