let size be non zero Nat; :: thesis: 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 holds
for m, n being Nat st ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size holds
val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let V, A be set ; :: thesis: for val being Function
for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size holds
val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let val be Function; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size holds
val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size holds
val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let d1 be NonatomicND of V,A; :: thesis: ( loc,val,size are_correct_wrt d1 implies for m, n being Nat st ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size holds
val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
assume A1: loc,val,size are_correct_wrt d1 ; :: thesis: for m, n being Nat st ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size holds
val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
then A2: val is_valid_wrt d1 ;
let m, n be Nat; :: thesis: ( ( n in dom val or ( 1 <= n & n <= size ) ) & 1 <= m & m <= size implies val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
assume A3: ( n in dom val or ( 1 <= n & n <= size ) ) ; :: thesis: ( not 1 <= m or not m <= size or val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )

now :: thesis: ( 1 <= n & n <= size implies n in dom val )

assume A4: ( 1 <= n & n <= size ) ; :: thesis: n in dom val
A5: dom (LocalOverlapSeq (A,loc,val,d1,size)) c= dom val by A1;
len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;
hence n in dom val by A5, A4, FINSEQ_3:25; :: thesis: verum

end;

then A6: val . n in rng val by A3, FUNCT_1:def 3;
assume ( 1 <= m & m <= size ) ; :: thesis: val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
then dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) by A1, Th7;
hence val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) by A2, A6; :: thesis: verum