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 & Seg size c= dom loc & loc | (Seg size) is one-to-one holds
for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j)
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 & Seg size c= dom loc & loc | (Seg size) is one-to-one holds
for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j)
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 & Seg size c= dom loc & loc | (Seg size) is one-to-one holds
for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j)
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 & Seg size c= dom loc & loc | (Seg size) is one-to-one holds
for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j)
let d1 be NonatomicND of V,A; :: thesis: ( loc,val,size are_correct_wrt d1 & Seg size c= dom loc & loc | (Seg size) is one-to-one implies for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
assume A1: loc,val,size are_correct_wrt d1 ; :: thesis: ( not Seg size c= dom loc or not loc | (Seg size) is one-to-one or for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j) )
assume A2: ( Seg size c= dom loc & loc | (Seg size) is one-to-one ) ; :: thesis: for j, m, n being Nat st 1 <= j & j <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j)
let j, m, n be Nat; :: thesis: ( 1 <= j & j <= n & n <= m & m <= size implies ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j) )
assume that
A3: 1 <= j and
A4: j <= n and
A5: n <= m and
A6: m <= size ; :: thesis: ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. j)
A7: 1 <= n by A3, A4, XXREAL_0:2;
set lo = loc /. j;
defpred S₁[ Nat] means ( n <= $1 & $1 <= size implies ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . $1) . (loc /. j) );
A8: S₁[ 0 ] ;
A9: 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
A10: S₁[k] and
A11: n <= k + 1 and
A12: k + 1 <= size ; :: thesis: ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. j)

per cases ( n <= k or n = k + 1 ) by A11, NAT_1:8;

suppose A13: n <= k ; :: thesis: ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. j)

then A14: 1 <= k by A7, XXREAL_0:2;
A15: k + 0 < k + 1 by XREAL_1:8;
then A16: k < size by A12, XXREAL_0:2;
A17: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;
set D = denaming (V,A,(val . (k + 1)));
reconsider d2 = (LocalOverlapSeq (A,loc,val,d1,size)) . k as NonatomicND of V,A by A14, A16, A17, Def6;
A18: dom (denaming (V,A,(val . (k + 1)))) = { d where d is NonatomicND of V,A : val . (k + 1) in dom d } by NOMIN_1:def 18;
A19: 1 <= k + 1 by NAT_1:12;
then val . (k + 1) in dom d2 by A1, A12, A14, A16, Th10;
then d2 in dom (denaming (V,A,(val . (k + 1)))) by A18;
then reconsider Dd2 = (denaming (V,A,(val . (k + 1)))) . d2 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A20: (LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1) = local_overlapping (V,A,d2,Dd2,(loc /. (k + 1))) by A14, A16, A17, Def4;
A21: j <= k + 0 by A4, A13, XXREAL_0:2;
j <= m by A4, A5, XXREAL_0:2;
then A22: j <= size by A6, XXREAL_0:2;
loc /. j in dom d2 by A1, A3, A16, A21, Th9;
hence ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. j) by A10, A13, A15, A1, A20, A22, A2, Th1, A3, A12, A21, A19, NOMIN_5:3, XXREAL_0:2; :: thesis: verum

end;

suppose n = k + 1 ; :: thesis: ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. j)

hence ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (loc /. j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. j) ; :: thesis: verum

end;

end;

end;

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