theorem Th14: :: NOMIN_7:14

for size being non zero Nat
for V, A being set
for loc being b₂ -valued Function
for d1 being NonatomicND of V,A
for val being b₁ -element FinSequence st loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= m & m <= size & 1 <= n & n <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (val . n) = d1 . (val . n)