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

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

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

val . n <> loc /. 1 by A1, A5, A6, A9;
hence ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (val . n) = d1 . (val . n) by A2, A16, A17, A18, A19, NOMIN_5:3; :: thesis: verum

end;

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

then A20: 0 + 1 <= k by NAT_1:13;
A21: k < size by A14, 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 A20, A8, A21, Def6;
A22: 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;
val . (k + 1) in dom d2 by A2, A13, A14, A20, A21, Th10;
then d2 in dom (denaming (V,A,(val . (k + 1)))) by A22;
then reconsider T = (denaming (V,A,(val . (k + 1)))) . d2 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A23: (LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1) = local_overlapping (V,A,d2,T,(loc /. (k + 1))) by A20, A8, A21, Def4;
A24: loc /. (k + 1) <> val . n by A1, A5, A6, A13, A14;
val . n in dom d2 by A2, A5, A6, A20, A21, Th10;
hence ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) . (val . n) = d1 . (val . n) by A2, A24, A23, A12, A20, A14, NAT_1:13, NOMIN_5:3; :: thesis: verum

end;

end;

end;

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