theorem Th20: :: NOMIN_8:20

for n, m being Nat
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 1 <= n & n <= len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m in dom (prg . n) holds
(prg . n) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) is TypeSCNominativeData of V,A