scheme :: MSUALG_8:sch 1
NonUniqSeqEx{ F₁() -> Element of NAT , P₁[ object , object ] } :

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

provided

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