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 S1[ 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: S1[ 0 ] ;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume that
A5: S1[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 S1[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