scheme :: RECDEF_1:sch 4
FinRecExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, P₁[ object , object , object ] } :

ex p being FinSequence of F₁() st
( len p = F₃() & ( p . 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,p . n,p . (n + 1)] ) )

provided

A1: for n being Nat st 1 <= n & n < F₃() holds
for x being Element of F₁() ex y being Element of F₁() st P₁[n,x,y]