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 not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n))
let V, A be set ; :: thesis: for val being Function
for loc being V -valued Function
for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n))
let val be Function; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n))
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n))
let d1 be NonatomicND of V,A; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V implies for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)) )
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V ; :: thesis: for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n))
let n be Nat; :: thesis: ( 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) implies dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)) )
assume that
A3: 1 <= n and
A4: n < size ; :: thesis: ( not val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) or dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
set X1 = (LocalOverlapSeq (A,loc,val,d1,size)) . n;
set X2 = (LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1);
assume A5: val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) ; :: thesis: dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n))
A6: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;
set v = loc /. (n + 1);
set D = denaming (V,A,(val . (n + 1)));
A7: dom (denaming (V,A,(val . (n + 1)))) = { d where d is NonatomicND of V,A : val . (n + 1) in dom d } by NOMIN_1:def 18;
reconsider X1 = (LocalOverlapSeq (A,loc,val,d1,size)) . n as NonatomicND of V,A by A3, A4, A6, Def6;
X1 in dom (denaming (V,A,(val . (n + 1)))) by A5, A7;
then reconsider d2 = (denaming (V,A,(val . (n + 1)))) . X1 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
(LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1) = local_overlapping (V,A,X1,d2,(loc /. (n + 1))) by A3, A4, A6, Def4;
hence dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)) by A1, A2, NOMIN_4:4; :: thesis: verum