let size be non zero Nat; for V, A being set
for val being Function
for loc being b1 -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 ; 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; 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; 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; ( 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
; 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; ( ( 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 ) )
; ( not 1 <= m or not m <= size or val . n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
now ( 1 <= n & n <= size implies n in dom val )assume A4:
( 1
<= n &
n <= size )
;
n in dom valA5:
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;
verum end;
then A6:
val . n in rng val
by A3, FUNCT_1:def 3;
assume
( 1 <= m & m <= size )
; 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; verum