scheme :: STIRL2_1:sch 5
Sch6{ F₁() -> non empty set , F₂() -> Nat, P₁[ object , object ] } :

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

provided

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