scheme :: LOPBAN_6:sch 1
RecExD3{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), P₁[ object , object , object , object ] } :

ex f being sequence of F₁() st
( f . 0 = F₂() & f . 1 = F₃() & ( for n being Nat holds P₁[n,f . n,f . (n + 1),f . (n + 2)] ) )

provided

A1: for n being Nat
for x, y being Element of F₁() ex z being Element of F₁() st P₁[n,x,y,z]