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 Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
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 Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A
for val being size -element FinSequence st Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let d1 be NonatomicND of V,A; :: thesis: for val being size -element FinSequence st Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 holds
for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let val be size -element FinSequence; :: thesis: ( Seg size c= dom loc & loc | (Seg size) is one-to-one & loc,val are_different_wrt size & loc,val,size are_correct_wrt d1 implies for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n) )
assume that
A1: Seg size c= dom loc and
A2: loc | (Seg size) is one-to-one and
A3: loc,val are_different_wrt size and
A4: loc,val,size are_correct_wrt d1 ; :: thesis: for m, n being Nat st 1 <= n & n <= m & m <= size holds
((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
let m, n be Nat; :: thesis: ( 1 <= n & n <= m & m <= size implies ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n) )
assume that
A5: 1 <= n and
A6: n <= m and
A7: m <= size ; :: thesis: ((LocalOverlapSeq (A,loc,val,d1,size)) . m) . (loc /. n) = d1 . (val . n)
set F = LocalOverlapSeq (A,loc,val,d1,size);
A8: Seg size = dom val by FINSEQ_1:89;
A9: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;
A10: 0 + 1 <= size by NAT_1:13;
A11: n <= size by A6, A7, XXREAL_0:2;
defpred S₁[ Nat] means ( n <= $1 & $1 <= size implies ((LocalOverlapSeq (A,loc,val,d1,size)) . $1) . (loc /. n) = d1 . (val . n) );
A12: S₁[ 0 ] by A5;
A13: 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
A14: S₁[k] and
A15: n <= k + 1 and
A16: k + 1 <= size ; :: thesis: ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n)
set D1 = denaming (V,A,(val . 1));
A17: dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d } by NOMIN_1:def 18;
A18: rng val c= dom d1 by A4, Def1;
1 in Seg size by A10, FINSEQ_1:1;
then A19: val . 1 in rng val by A8, FUNCT_1:def 3;
then d1 in dom (denaming (V,A,(val . 1))) by A18, A17;
then reconsider T1 = (denaming (V,A,(val . 1))) . d1 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A20: (LocalOverlapSeq (A,loc,val,d1,size)) . 1 = local_overlapping (V,A,d1,T1,(loc /. 1)) by Def4;
n in Seg size by A5, A11, FINSEQ_1:1;
then A21: val . n in rng val by A8, FUNCT_1:def 3;

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

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

then n = 1 by A5, A15, XXREAL_0:1;
hence ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n) by A4, A19, A18, A20, A22, Th2; :: thesis: verum

end;

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

then A23: 0 + 1 <= k by NAT_1:13;
A24: 1 <= k + 1 by NAT_1:11;
A25: k < size by A16, NAT_1:13;
set D = denaming (V,A,(val . (k + 1)));
reconsider d2 = (LocalOverlapSeq (A,loc,val,d1,size)) . k as NonatomicND of V,A by A23, A9, A25, Def6;
A26: 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;
A27: val . (k + 1) in dom d2 by A4, A24, A16, A23, A25, Th10;
then d2 in dom (denaming (V,A,(val . (k + 1)))) by A26;
then reconsider T = (denaming (V,A,(val . (k + 1)))) . d2 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A28: (LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1) = local_overlapping (V,A,d2,T,(loc /. (k + 1))) by A23, A9, A25, Def4;

per cases ( k + 1 = n or k + 1 <> n ) ;

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

then A30: k < n by NAT_1:13;
1 < n by A23, A29, NAT_1:13;
then A31: loc /. 1 <> val . n by A3, A10, A11;
thus ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d2 . (val . n) by A4, A29, A27, A28, Th2
.= ((LocalOverlapSeq (A,loc,val,d1,size)) . 1) . (val . n) by A4, A3, A11, A23, A30, Th11
.= d1 . (val . n) by A4, A18, A20, A31, A21, NOMIN_5:3 ; :: thesis: verum

end;

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

then A32: n < k + 1 by A15, XXREAL_0:1;
then n <= k by NAT_1:13;
then loc /. n in dom d2 by A4, A5, A25, Th9;
hence ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (loc /. n) = d1 . (val . n) by A1, A2, A5, A4, A11, A14, A16, A24, A28, A32, Th1, NAT_1:13, NOMIN_5:3; :: thesis: verum

end;

end;

end;

end;

end;

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