theorem Th17: :: NOMIN_8:17

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) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))