let n, m be Nat; :: thesis: for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b₅ -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 ; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b₃ -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; :: thesis: for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b₂ -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; :: thesis: for size being non zero Nat
for val being b₁ -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; :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: ( 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)) ) ; :: thesis: (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; :: thesis: verum