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