let n, m be Nat; for V, A being set
for loc being b1 -valued Function
for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b5 -element FinSequence st loc,val,size are_correct_wrt d1 & 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) & 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) holds
(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))
let V, A be set ; for loc being V -valued Function
for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b3 -element FinSequence st loc,val,size are_correct_wrt d1 & 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) & 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) holds
(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))
let loc be V -valued Function; for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b2 -element FinSequence st loc,val,size are_correct_wrt d1 & 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) & 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) holds
(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))
let d1 be NonatomicND of V,A; for size being non zero Nat
for val being b1 -element FinSequence st loc,val,size are_correct_wrt d1 & 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) & 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) holds
(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))
let size be non zero Nat; for val being size -element FinSequence st loc,val,size are_correct_wrt d1 & 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) & 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) holds
(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))
let val be size -element FinSequence; ( loc,val,size are_correct_wrt d1 & 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) & 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) implies (LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m))) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
set v = val . m;
assume that
A1:
loc,val,size are_correct_wrt d1
and
A2:
( 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) )
; ( not 1 <= m or not m <= len (LocalOverlapSeq (A,loc,val,d1,size)) or (LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m))) )
A3:
len (LocalOverlapSeq (A,loc,val,d1,size)) = size
by NOMIN_7:def 4;
A4:
dom (denaming (V,A,(val . m))) = { d where d is NonatomicND of V,A : val . m in dom d }
by NOMIN_1:def 18;
A5:
(LocalOverlapSeq (A,loc,val,d1,size)) . n is NonatomicND of V,A
by A2, NOMIN_7:def 6;
assume
( 1 <= m & m <= len (LocalOverlapSeq (A,loc,val,d1,size)) )
; (LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))
then
val . m in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
by A1, A2, A3, NOMIN_7:10;
hence
(LocalOverlapSeq (A,loc,val,d1,size)) . n in dom (denaming (V,A,(val . m)))
by A4, A5; verum