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

A15: now :: thesis: not k < 1

assume k < 1 ; :: thesis: contradiction
then k + 1 <= 1 by NAT_1:13;
then m <= 1 by A12, XXREAL_0:2;
hence contradiction by A5, A6, XXREAL_0:2; :: thesis: verum

end;

A16: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;
A17: k <= k + 1 by NAT_1:11;
A18: k <= size by A13, A17, XXREAL_0:2;
then reconsider d2 = (LocalOverlapSeq (A,loc,val,d1,size)) . k as NonatomicND of V,A by A15, A16, 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;
1 <= k + 1 by NAT_1:11;
then val . (k + 1) in dom d2 by A1, A13, A15, A18, Th10;
then d2 in dom (denaming (V,A,(val . (k + 1)))) by A19;
then reconsider T = (denaming (V,A,(val . (k + 1)))) . d2 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
set L = local_overlapping (V,A,d2,T,(loc /. (k + 1)));

per cases ( m <= k or m > k ) ;

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

hence ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. m) = ((LocalOverlapSeq (A,loc,val,d1,size)) . j) . (val . m) by A1, A2, A3, A11, A13, A17, A14, Th12, XXREAL_0:2; :: thesis: verum

end;

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

then k + 1 <= m by NAT_1:13;
then A20: m = k + 1 by A12, XXREAL_0:1;
A21: m <= size by A7, A8, XXREAL_0:2;
j <= size by A6, A21, XXREAL_0:2;
hence ((LocalOverlapSeq (A,loc,val,d1,size)) . j) . (val . m) = d1 . (val . m) by A1, A5, A4, A14, A21, Th14
.= ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. m) by A1, A2, A3, A4, A14, A20, A21, Th13 ;
:: thesis: verum

end;

end;

end;

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