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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for n being Nat st 1 <= n & n <= len prg holds
dom d1 c= 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for n being Nat st 1 <= n & n <= len prg holds
dom d1 c= 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for n being Nat st 1 <= n & n <= len prg holds
dom d1 c= 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for n being Nat st 1 <= n & n <= len prg holds
dom d1 c= 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos implies for n being Nat st 1 <= n & n <= len prg holds
dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) )
set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V and
A3: dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg and
A4: d1 in dom (prg . 1) and
A5: prg_doms_of loc,d1,prg,pos ; :: thesis: for n being Nat st 1 <= n & n <= len prg holds
dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)
let n be Nat; :: thesis: ( 1 <= n & n <= len prg implies dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) )
assume that
A6: 1 <= n and
A7: n <= len prg ; :: thesis: dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len prg implies dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . $1) );
A8: S₁[ 0 ] ;
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A10: S₁[k] and
A11: 1 <= k + 1 and
A12: k + 1 <= len prg ; :: thesis: dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1))
A13: len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) = len prg by Def14;

per cases ( k = 0 or k > 0 ) ;

suppose A14: k = 0 ; :: thesis: dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1))

set v = loc /. (pos . 1);
set D = prg . 1;
1 <= len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) by A11, A12, A13, XXREAL_0:2;
then 1 in dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) by FINSEQ_3:25;
then prg . 1 in rng prg by A3, FUNCT_1:def 3;
then reconsider d2 = (prg . 1) . d1 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39, A4;
A15: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . 1 = local_overlapping (V,A,d1,d2,(loc /. (pos . 1))) by A7, Def14;
dom (local_overlapping (V,A,d1,d2,(loc /. (pos . 1)))) = {(loc /. (pos . 1))} \/ (dom d1) by A1, A2, NOMIN_4:4;
hence dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1)) by A14, A15, XBOOLE_1:7; :: thesis: verum

end;

suppose k > 0 ; :: thesis: dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1))

then A16: 0 + 1 <= k by NAT_1:13;
A17: k <= k + 1 by NAT_1:12;
k + 0 < k + 1 by XREAL_1:8;
then A18: k < len prg by A12, XXREAL_0:2;
then (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . k in dom (prg . (k + 1)) by A5, A16;
then dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . k) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1)) by A1, A2, A16, A18, Th22;
hence dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1)) by A17, A10, A12, A16, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A9);
hence dom d1 c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) by A6, A7; :: thesis: verum