scheme :: POLYNOM3:sch 1
SeqOfSeqLambdaD{ F₁() -> non empty set , F₂() -> Element of NAT , F₃( Nat) -> Element of NAT , F₄( set , set ) -> Element of F₁() } :

ex p being FinSequence of F₁() * st
( len p = F₂() & ( for k being Element of NAT st k in Seg F₂() holds
( len (p /. k) = F₃(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F₄(k,n) ) ) ) )