theorem Th5: :: NOMIN_7:5

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 not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n))