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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
loc /. (pos . n) in 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
loc /. (pos . n) in 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
loc /. (pos . n) in 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos holds
for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
loc /. (pos . n) in 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 & dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg & d1 in dom (prg . 1) & prg_doms_of loc,d1,prg,pos implies for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) )
set size = len prg;
set F = PrgLocalOverlapSeq (A,loc,d1,prg,pos);
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V and
A3: dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) c= dom prg and
A4: d1 in dom (prg . 1) and
A5: prg_doms_of loc,d1,prg,pos ; :: thesis: for m, n being Nat st 1 <= n & n <= m & m <= len prg holds
loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
let m, n be Nat; :: thesis: ( 1 <= n & n <= m & m <= len prg implies loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) )
assume that
A6: 1 <= n and
A7: n <= m and
A8: m <= len prg ; :: thesis: loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
A9: 1 <= m by A6, A7, XXREAL_0:2;
A10: n <= len prg by A7, A8, XXREAL_0:2;
A11: len (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) = len prg by Def14;
reconsider i1 = n - 1 as Element of NAT by A6, INT_1:5;
set v = loc /. (pos . n);
set D = prg . n;
A12: loc /. (pos . n) in {(loc /. (pos . n))} by TARSKI:def 1;
n in dom (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) by A6, A10, A11, FINSEQ_3:25;
then A13: prg . n in rng prg by A3, FUNCT_1:def 3;
per cases ( i1 = 0 or i1 > 0 ) ;
suppose A14: i1 = 0 ; :: thesis: loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
then reconsider d2 = (prg . n) . d1 as TypeSCNominativeData of V,A by A4, A13, PARTFUN1:4, NOMIN_1:39;
A15: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . 1 = local_overlapping (V,A,d1,d2,(loc /. (pos . n))) by A8, A14, Def14;
A16: dom (local_overlapping (V,A,d1,d2,(loc /. (pos . n)))) = {(loc /. (pos . n))} \/ (dom d1) by A1, A2, NOMIN_4:4;
A17: dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . 1) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) by A1, A5, A2, A8, A9, Th24;
loc /. (pos . n) in {(loc /. (pos . n))} \/ (dom d1) by A12, XBOOLE_0:def 3;
hence loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) by A15, A16, A17; :: thesis: verum
end;
suppose i1 > 0 ; :: thesis: loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m)
then A18: 0 + 1 <= i1 by NAT_1:13;
n - 1 < n - 0 by XREAL_1:15;
then A19: i1 < len prg by A10, XXREAL_0:2;
then reconsider dd = (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . i1 as NonatomicND of V,A by A18, A11, NOMIN_7:def 6;
dd in dom (prg . (i1 + 1)) by A5, A18, A19;
then reconsider d2 = (prg . n) . dd as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39, A13;
A20: (PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n = local_overlapping (V,A,dd,d2,(loc /. (pos . (i1 + 1)))) by A11, A18, A19, Def14;
A21: dom (local_overlapping (V,A,dd,d2,(loc /. (pos . n)))) = {(loc /. (pos . n))} \/ (dom dd) by A1, A2, NOMIN_4:4;
A22: loc /. (pos . n) in {(loc /. (pos . n))} \/ (dom dd) by A12, XBOOLE_0:def 3;
dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . n) c= dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) by A1, A5, A2, A6, A7, A8, Th24;
hence loc /. (pos . n) in dom ((PrgLocalOverlapSeq (A,loc,d1,prg,pos)) . m) by A22, A20, A21; :: thesis: verum
end;
end;