let size be non zero Nat; :: thesis: for V, A being set
for val being Function
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let V, A be set ; :: thesis: for val being Function
for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let val be Function; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let d1 be NonatomicND of V,A; :: thesis: ( loc,val,size are_correct_wrt d1 implies for m, n being Nat st 1 <= n & n <= m & m <= size holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
assume A1: loc,val,size are_correct_wrt d1 ; :: thesis: for m, n being Nat st 1 <= n & n <= m & m <= size holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
let m, n be Nat; :: thesis: ( 1 <= n & n <= m & m <= size implies dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
assume that
A2: 1 <= n and
A3: n <= m and
A4: m <= size ; :: thesis: dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)

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

suppose n = m ; :: thesis: dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)

hence dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) ; :: thesis: verum

end;

suppose A5: n < m ; :: thesis: dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)

defpred S₁[ Nat] means ( n < $1 & $1 <= size implies dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . $1) );
A6: S₁[ 0 ] ;
A7: 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
A8: S₁[k] and
A9: n < k + 1 and
A10: k + 1 <= size ; :: thesis: dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))
A11: n <= k by A9, NAT_1:13;
then A12: 1 <= k by A2, XXREAL_0:2;
k + 0 < k + 1 by XREAL_1:8;
then A13: k < size by A10, XXREAL_0:2;
len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;
then k + 1 in dom (LocalOverlapSeq (A,loc,val,d1,size)) by A10, FINSEQ_3:25, NAT_1:12;
then A14: val . (k + 1) in rng val by A1, FUNCT_1:def 3;
A15: val is_valid_wrt d1 by A1;
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . k) by A1, A12, A13, Th7;
then dom ((LocalOverlapSeq (A,loc,val,d1,size)) . k) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) by A1, A15, A12, A13, A14, Th6;
hence dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) by A8, A11, A10, NAT_1:13, XXREAL_0:1; :: thesis: verum

end;

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

end;

end;