scheme :: RECDEF_1:sch 17
SeqExD{ F₁() -> non empty set , F₂() -> Nat, P₁[ object , object ] } :

ex p being FinSequence of F₁() st
( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p /. k] ) )

provided

A1: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₁[k,x]