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

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

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

then A15: 1 <= k by A3, XXREAL_0:2;
A16: k + 1 < size by A12, A13, XXREAL_0:2;
then A17: k < size by NAT_1:13;
A18: 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 A15, A17, A18, Def6;
A19: 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;
A20: 1 <= k + 1 by NAT_1:12;
val . (k + 1) in dom d2 by A1, A15, A17, A20, A16, Th10;
then d2 in dom (denaming (V,A,(val . (k + 1)))) by A19;
then reconsider Dd2 = (denaming (V,A,(val . (k + 1)))) . d2 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A21: (LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1) = local_overlapping (V,A,d2,Dd2,(loc /. (k + 1))) by A15, A17, A18, Def4;
A22: k + 0 < k + 1 by XREAL_1:8;
A23: 1 <= j by A5, A7, XXREAL_0:2;
then A24: loc /. (k + 1) <> val . j by A2, A13, A20, A16;
val . j in dom d2 by A1, A15, A17, A23, A13, Th10;
hence ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (val . j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (val . j) by A10, A14, A13, A22, A12, A1, A21, A24, NOMIN_5:3, XXREAL_0:2; :: thesis: verum

end;

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

hence ((LocalOverlapSeq (A,loc,val,d1,size)) . n) . (val . j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (val . 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) . (val . j) = ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (val . j) by A4, A5, A6; :: thesis: verum