scheme :: FIELD_12:sch 1
RecExField{ F₁() -> Field, P₁[ object , Field, Field] } :

ex f being Field-yielding sequence st
( f . 0 = F₁() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )

provided

A1: for n being Nat
for x being Field ex y being Field st P₁[n,x,y]