set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);
A1: len prg > 0 ;
let n be Nat; :: according to NOMIN_7:def 6 :: thesis: ( not 1 <= n or not n <= len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) or (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is NonatomicND of V,A )
assume A2: ( 1 <= n & n <= len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) ) ; :: thesis: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is NonatomicND of V,A
set X = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1)));
defpred S₁[ Nat] means ( 1 <= V & V <= len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) implies (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . V is NonatomicND of V,A );
A3: S₁[ 0 ] ;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A5: S₁[n] and
1 <= n + 1 and
A6: n + 1 <= len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) ; :: thesis: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1) is NonatomicND of V,A

per cases ( n = 0 or 0 < n ) ;

suppose A7: n = 0 ; :: thesis: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1) is NonatomicND of V,A

(PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) by A1, Def14;
hence (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1) is NonatomicND of V,A by A7, NOMIN_2:9; :: thesis: verum

end;

suppose 0 < n ; :: thesis: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1) is NonatomicND of V,A

then A8: 0 + 1 <= n by NAT_1:13;
A9: n + 0 < n + 1 by XREAL_1:8;
then n < len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) by A6, XXREAL_0:2;
then (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1) = local_overlapping (V,A,((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n),((prg . (n + 1)) . ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n)),(loc /. (pos . (n + 1)))) by A1, A8, Def14;
hence (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (n + 1) is NonatomicND of V,A by A5, A6, A8, A9, NOMIN_2:9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n is NonatomicND of V,A by A2; :: thesis: verum