let V, A be set ; 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; 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; 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; 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; ( 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
; 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; ( 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))
; 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; verum