theorem Th12: :: NOMIN_7:12

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 & Seg size c= dom loc & loc | (Seg size) is one-to-one holds
for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j)