theorem Th16: :: NOMIN_8:16

for n being Nat
for V, A being set
for loc being b₂ -valued Function
for d1 being NonatomicND of V,A
for p being SCPartialNominativePredicate of V,A
for d being object
for size being non zero Nat
for val being b₈ -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & 2 <= n + 1 & n + 1 < size & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - n) - 1)),((denaming (V,A,(val . ((len val) - n)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . ((size - n) - 1))),(loc /. ((len val) - n))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . n)