theorem Th15: :: NOMIN_8:15

for n, m being Nat
for V, A being set
for loc being b₃ -valued Function
for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b₇ -element FinSequence st loc,val,size are_correct_wrt d1 & 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) & 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) holds
(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))