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 & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
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 & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
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 & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
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 & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
let prg be non empty FPrg (ND (V,A)) -valued FinSequence; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V & prg_doms_of loc,d1,prg,pos implies for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) )
set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);
assume that
A1: ( not V is empty & A is_without_nonatomicND_wrt V ) and
A2: prg_doms_of loc,d1,prg,pos ; :: thesis: for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
let m, n be Nat; :: thesis: ( 1 <= n & n <= m & m <= len prg implies dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) )
assume that
A3: 1 <= n and
A4: n <= m and
A5: m <= len prg ; :: thesis: dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)

per cases ( n = m or n < m ) by A4, XXREAL_0:1;

suppose n = m ; :: thesis: dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)

hence dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) ; :: thesis: verum

end;

suppose A6: n < m ; :: thesis: dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)

defpred S₁[ Nat] means ( n < $1 & $1 <= len prg implies dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . $1) );
A7: S₁[ 0 ] ;
A8: 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
A9: S₁[k] and
A10: n < k + 1 and
A11: k + 1 <= len prg ; :: thesis: dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1))
A12: n <= k by A10, NAT_1:13;
then A13: 1 <= k by A3, XXREAL_0:2;
k + 0 < k + 1 by XREAL_1:8;
then A14: k < len prg by A11, XXREAL_0:2;
then (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . k in dom (prg . (k + 1)) by A2, A13;
then dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . k) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1)) by A1, A13, A14, Th22;
hence dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . (k + 1)) by A9, A12, A11, NAT_1:13, XXREAL_0:1; :: thesis: verum

end;

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

end;

end;