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 & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)