scheme :: YELLOW15:sch 1
SeqLambda1C{ F₁() -> Nat, F₂() -> non empty set , P₁[ object ], F₃( object ) -> set , F₄( object ) -> set } :

ex p being FinSequence of F₂() st
( len p = F₁() & ( for i being Nat st i in Seg F₁() holds
( ( P₁[i] implies p . i = F₃(i) ) & ( P₁[i] implies p . i = F₄(i) ) ) ) )

provided

A1: for i being Nat st i in Seg F₁() holds
( ( P₁[i] implies F₃(i) in F₂() ) & ( P₁[i] implies F₄(i) in F₂() ) )