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 size being non zero Nat
for val being b₆ -element FinSequence
for dx, dy being object
for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)