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
loc /. n in 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
loc /. n in 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
loc /. n in 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
loc /. n in 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
loc /. n in 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
loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
then A2: val is_valid_wrt d1 ;
let m, n be Nat; :: thesis: ( 1 <= n & n <= m & m <= size implies loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) )
assume that
A3: 1 <= n and
A4: n <= m and
A5: m <= size ; :: thesis: loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)
A6: 1 <= m by A3, A4, XXREAL_0:2;
A7: n <= size by A4, A5, XXREAL_0:2;
A8: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;
reconsider i1 = n - 1 as Element of NAT by A3, INT_1:5;
set v = loc /. n;
set D = denaming (V,A,(val . n));
A9: dom (denaming (V,A,(val . n))) = { d where d is NonatomicND of V,A : val . n in dom d } by NOMIN_1:def 18;
A10: loc /. n in {(loc /. n)} by TARSKI:def 1;
n in dom (LocalOverlapSeq (A,loc,val,d1,size)) by A3, A7, A8, FINSEQ_3:25;
then A11: val . n in rng val by A1, FUNCT_1:def 3;
then A12: val . n in dom d1 by A2;

per cases ( i1 = 0 or i1 > 0 ) ;

suppose A13: i1 = 0 ; :: thesis: loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)

d1 in dom (denaming (V,A,(val . n))) by A2, A9, A11;
then reconsider d2 = (denaming (V,A,(val . n))) . d1 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A14: (LocalOverlapSeq (A,loc,val,d1,size)) . 1 = local_overlapping (V,A,d1,d2,(loc /. n)) by A13, Def4;
A15: dom (local_overlapping (V,A,d1,d2,(loc /. n))) = {(loc /. n)} \/ (dom d1) by A1, NOMIN_4:4;
A16: dom ((LocalOverlapSeq (A,loc,val,d1,size)) . 1) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) by A1, A5, A6, Th8;
loc /. n in {(loc /. n)} \/ (dom d1) by A10, XBOOLE_0:def 3;
hence loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) by A14, A15, A16; :: thesis: verum

end;

suppose i1 > 0 ; :: thesis: loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m)

then A17: 0 + 1 <= i1 by NAT_1:13;
n - 1 < n - 0 by XREAL_1:15;
then A18: i1 < size by A7, XXREAL_0:2;
then reconsider dd = (LocalOverlapSeq (A,loc,val,d1,size)) . i1 as NonatomicND of V,A by A17, A8, Def6;
dom d1 c= dom dd by A1, A17, A18, Th7;
then dd in dom (denaming (V,A,(val . n))) by A12, A9;
then reconsider d2 = (denaming (V,A,(val . n))) . dd as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A19: (LocalOverlapSeq (A,loc,val,d1,size)) . n = local_overlapping (V,A,dd,d2,(loc /. (i1 + 1))) by A8, A17, A18, Def4;
A20: dom (local_overlapping (V,A,dd,d2,(loc /. n))) = {(loc /. n)} \/ (dom dd) by A1, NOMIN_4:4;
A21: loc /. n in {(loc /. n)} \/ (dom dd) by A10, XBOOLE_0:def 3;
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) by A1, A3, A4, A5, Th8;
hence loc /. n in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . m) by A21, A19, A20; :: thesis: verum

end;

end;