let V, A be set ; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A
for pos being FinSequence
for prg being non empty FPrg (ND (V,A)) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n))
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A
for pos being FinSequence
for prg being non empty FPrg (ND (V,A)) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n))
let d1 be NonatomicND of V,A; :: thesis: for pos being FinSequence
for prg being non empty FPrg (ND (V,A)) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n))
let pos be FinSequence; :: thesis: for prg being non empty FPrg (ND (V,A)) -valued FinSequence st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n))
let prg be non empty FPrg (ND (V,A)) -valued FinSequence; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V implies for n being Nat st 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)) )
set size = len prg;
set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V ; :: thesis: for n being Nat st 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n))
let n be Nat; :: thesis: ( 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) implies dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)) )
assume that
A3: 1 <= n and
A4: n < len prg and
A5: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) ; :: thesis: dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n))
A6: len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) = len prg by Def14;
reconsider Fn = (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n as NonatomicND of V,A by A3, A4, A6, NOMIN_7:def 6;
set v = loc /. (pos . (n + 1));
set d2 = (prg . (n + 1)) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n);
n + 1 <= len prg by A4, NAT_1:13;
then (prg . (n + 1)) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) is TypeSCNominativeData of V,A by A5, NAT_1:11, Th20;
then dom (local_overlapping (V,A,Fn,((prg . (n + 1)) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)),(loc /. (pos . (n + 1))))) = {(loc /. (pos . (n + 1)))} \/ (dom Fn) by A1, A2, NOMIN_4:4;
hence dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)) by A3, A4, A6, Def14; :: thesis: verum