theorem Th21: :: NOMIN_8:21

for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A
for pos being FinSequence
for prg being non empty FPrg (ND (b₁,b₂)) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n))