:: deftheorem Def9 defines SC_Psuperpos_Seq NOMIN_8:def 9 :
for V, A being set
for loc being b₁ -valued Function
for val being FinSequence st len val > 0 holds
for p being SCPartialNominativePredicate of V,A
for b₆ being FinSequence of PFuncs ((ND (V,A)),BOOLEAN) holds
( b₆ = SC_Psuperpos_Seq (loc,val,p) iff ( len b₆ = len val & b₆ . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) & ( for n being Nat st 1 <= n & n < len b₆ holds
b₆ . (n + 1) = SC_Psuperpos ((b₆ . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) ) );