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) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1))
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) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1))
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) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1))
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) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1))
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) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) )
set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);
assume A1: ( not V is empty & 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) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1))
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) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) )
assume ( 1 <= n & n < len prg & (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n in dom (prg . (n + 1)) ) ; :: thesis: dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1))
then dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) = {(loc /. (pos . (n + 1)))} \/ (dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)) by A1, Th21;
hence dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1)) by XBOOLE_1:7; :: thesis: verum