:: deftheorem Def4 defines LocalOverlapSeq NOMIN_7:def 4 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for d1 being NonatomicND of V,A
for size being Nat st size > 0 holds
for b₇ being FinSequence of ND (V,A) holds
( b₇ = LocalOverlapSeq (A,loc,val,d1,size) iff ( len b₇ = size & b₇ . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b₇ holds
b₇ . (n + 1) = local_overlapping (V,A,(b₇ . n),((denaming (V,A,(val . (n + 1)))) . (b₇ . n)),(loc /. (n + 1))) ) ) );