set F = LocalOverlapSeq (A,loc,val,d1,size);
let n be Nat; :: according to NOMIN_7:def 6 :: thesis: ( 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) implies (LocalOverlapSeq (A,loc,val,d1,size)) . n is NonatomicND of V,A )
assume A1: ( 1 <= n & n <= len (LocalOverlapSeq (A,loc,val,d1,size)) ) ; :: thesis: (LocalOverlapSeq (A,loc,val,d1,size)) . n is NonatomicND of V,A
set X = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1));
defpred S₁[ Nat] means ( 1 <= V & V <= len (LocalOverlapSeq (A,loc,val,d1,size)) implies (LocalOverlapSeq (A,loc,val,d1,size)) . V is NonatomicND of V,A );
A2: S₁[ 0 ] ;
A3: 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
A4: S₁[n] and
1 <= n + 1 and
A5: n + 1 <= len (LocalOverlapSeq (A,loc,val,d1,size)) ; :: thesis: (LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1) is NonatomicND of V,A

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

suppose A6: n = 0 ; :: thesis: (LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1) is NonatomicND of V,A

(LocalOverlapSeq (A,loc,val,d1,size)) . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) by Def4;
hence (LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1) is NonatomicND of V,A by A6, NOMIN_2:9; :: thesis: verum

end;

suppose 0 < n ; :: thesis: (LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1) is NonatomicND of V,A

then A7: 0 + 1 <= n by NAT_1:13;
A8: n + 0 < n + 1 by XREAL_1:8;
then n < len (LocalOverlapSeq (A,loc,val,d1,size)) by A5, XXREAL_0:2;
then (LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . n),((denaming (V,A,(val . (n + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . n)),(loc /. (n + 1))) by A7, Def4;
hence (LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1) is NonatomicND of V,A by A4, A5, A7, A8, NOMIN_2:9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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