scheme :: RECDEF_1:sch 7
FinRecUn{ F₁() -> object , F₂() -> Nat, F₃() -> FinSequence, F₄() -> FinSequence, P₁[ object , object , object ] } :

F₃() = F₄()

provided

A1: for n being Nat st 1 <= n & n < F₂() holds
for x, y1, y2 being set 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)] ) )