scheme :: AFINSQ_1:sch 1
XSeqEx{ F₁() -> Nat, P₁[ object , object ] } :

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

provided

A1: for k being Nat st k in F₁() holds
ex x being object st P₁[k,x]