let V, A be set ; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A
for p being SCPartialNominativePredicate of V,A
for d being object
for size being non zero Nat
for val being b₅ -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A
for p being SCPartialNominativePredicate of V,A
for d being object
for size being non zero Nat
for val being b₄ -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
let d1 be NonatomicND of V,A; :: thesis: for p being SCPartialNominativePredicate of V,A
for d being object
for size being non zero Nat
for val being b₃ -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
let p be SCPartialNominativePredicate of V,A; :: thesis: for d being object
for size being non zero Nat
for val being b₂ -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
let d be object ; :: thesis: for size being non zero Nat
for val being b₁ -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
let size be non zero Nat; :: thesis: for val being size -element FinSequence st loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p holds
for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
let val be size -element FinSequence; :: thesis: ( loc,val,size are_correct_wrt d1 & d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p implies for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n)) )
assume that
A1: loc,val,size are_correct_wrt d1 and
A2: d = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) and
A3: local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p ; :: thesis: for m, n being Nat st 1 <= m & m < size & 1 <= n & n < size holds
((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
let m, n be Nat; :: thesis: ( 1 <= m & m < size & 1 <= n & n < size implies ((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n)) )
assume that
A4: 1 <= m and
A5: m < size and
A6: 1 <= n and
A7: n < size ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . n) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - n))
set S = SC_Psuperpos_Seq (loc,val,p);
set L = LocalOverlapSeq (A,loc,val,d1,size);
defpred S₁[ Nat] means ( 1 <= $1 & $1 < size implies ((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . $1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - $1)) );
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
1 <= k + 1 and
A11: k + 1 < size ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . (k + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (k + 1)))
set D = denaming (V,A,(val . ((len val) - k)));
A12: len val = size by CARD_1:def 7;
A13: len (SC_Psuperpos_Seq (loc,val,p)) = len val by Def9;
A14: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by NOMIN_7:def 4;
A15: k < size by A11, NAT_1:13;

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

suppose A16: k = 0 ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . (k + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (k + 1)))

defpred S₂[ Nat] means ( 1 <= $1 & $1 < size implies ((SC_Psuperpos_Seq (loc,val,p)) . $1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - $1)) = ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) );
A17: S₂[ 0 ] ;
A18: for x being Nat st S₂[x] holds
S₂[x + 1]

proof

let x be Nat; :: thesis: ( S₂[x] implies S₂[x + 1] )
assume that
A19: S₂[x] and
1 <= x + 1 and
A20: x + 1 < size ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . (x + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (x + 1))) = ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1))

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

suppose x = 0 ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . (x + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (x + 1))) = ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1))

hence ((SC_Psuperpos_Seq (loc,val,p)) . (x + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (x + 1))) = ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) ; :: thesis: verum

end;

suppose x > 0 ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . (x + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (x + 1))) = ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1))

then A21: 0 + 1 <= x by NAT_1:13;
set DD = denaming (V,A,(val . ((len val) - x)));
A22: x <= x + 1 by NAT_1:11;
then x < len (SC_Psuperpos_Seq (loc,val,p)) by A13, A12, A20, XXREAL_0:2;
then A23: (SC_Psuperpos_Seq (loc,val,p)) . (x + 1) = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . x),(denaming (V,A,(val . ((len val) - x)))),(loc /. ((len val) - x))) by A21, Def9;
reconsider u = (size - x) - 1 as Element of NAT by A20, XREAL_1:19, INT_1:5;
(x + 1) - x < size - x by A20, XREAL_1:9;
then 1 - 1 < (size - x) - 1 by XREAL_1:9;
then A24: 0 + 1 <= size - (x + 1) by INT_1:7;
A25: size - (x + 1) < size by XREAL_1:44;
then reconsider dd = (LocalOverlapSeq (A,loc,val,d1,size)) . u as NonatomicND of V,A by A14, A24, NOMIN_7:def 6;
A26: dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . x),(denaming (V,A,(val . ((len val) - x)))),(loc /. ((len val) - x)))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . ((len val) - x)))) . d),(loc /. ((len val) - x))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . x) & d in dom (denaming (V,A,(val . ((len val) - x)))) ) } by NOMIN_2:def 11;
1 + 1 <= x + 1 by A21, XREAL_1:6;
then A27: local_overlapping (V,A,dd,((denaming (V,A,(val . ((len val) - x)))) . dd),(loc /. ((len val) - x))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . x) by A1, A2, A3, A20, Th16;
A28: dom (denaming (V,A,(val . ((len val) - x)))) = { d where d is NonatomicND of V,A : val . ((len val) - x) in dom d } by NOMIN_1:def 18;
A29: 1 <= u + 1 by NAT_1:11;
u + 1 <= size by A25, INT_1:7;
then val . (u + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . u) by A1, A24, A25, A29, NOMIN_7:10;
then dd in dom (denaming (V,A,(val . ((len val) - x)))) by A12, A28;
then A30: dd in dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . x),(denaming (V,A,(val . ((len val) - x)))),(loc /. ((len val) - x)))) by A26, A27;
(LocalOverlapSeq (A,loc,val,d1,size)) . (u + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . u),((denaming (V,A,(val . (u + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . u)),(loc /. (u + 1))) by A14, A24, A25, NOMIN_7:def 4;
hence ((SC_Psuperpos_Seq (loc,val,p)) . (x + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (x + 1))) = ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) by A22, A23, A30, A12, A19, A21, A20, XXREAL_0:2, NOMIN_2:35; :: thesis: verum

end;

end;

end;

for x being Nat holds S₂[x] from NAT_1:sch 2(A17, A18);
hence ((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . (k + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (k + 1))) by A4, A5, A16; :: thesis: verum

end;

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

then A31: 0 + 1 <= k by NAT_1:13;
then A32: (SC_Psuperpos_Seq (loc,val,p)) . (k + 1) = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . k),(denaming (V,A,(val . ((len val) - k)))),(loc /. (size - k))) by A12, A13, A15, Def9;
set D1 = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - (k + 1));
A33: (k + 1) - k < size - k by A11, XREAL_1:9;
then reconsider w = (size - k) - 1 as Element of NAT by INT_1:5;
1 - 1 < w by A33, XREAL_1:9;
then A34: 0 + 1 <= w by NAT_1:13;
A35: size - (k + 1) < size by XREAL_1:44;
then A36: (LocalOverlapSeq (A,loc,val,d1,size)) . (w + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . w),((denaming (V,A,(val . (w + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . w)),(loc /. (w + 1))) by A14, A34, NOMIN_7:def 4;
reconsider D1 = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - (k + 1)) as NonatomicND of V,A by A14, A34, A35, NOMIN_7:def 6;
A37: dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . k),(denaming (V,A,(val . ((len val) - k)))),(loc /. ((len val) - k)))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . ((len val) - k)))) . d),(loc /. ((len val) - k))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . k) & d in dom (denaming (V,A,(val . ((len val) - k)))) ) } by NOMIN_2:def 11;
A38: D1 = (LocalOverlapSeq (A,loc,val,d1,size)) . ((size - k) - 1) ;
1 + 1 <= k + 1 by A31, XREAL_1:6;
then A39: local_overlapping (V,A,D1,((denaming (V,A,(val . ((len val) - k)))) . D1),(loc /. ((len val) - k))) in dom ((SC_Psuperpos_Seq (loc,val,p)) . k) by A1, A11, A2, A3, A38, Th16;
A40: dom (denaming (V,A,(val . ((len val) - k)))) = { d where d is NonatomicND of V,A : val . ((len val) - k) in dom d } by NOMIN_1:def 18;
A41: 1 <= w + 1 by NAT_1:11;
w + 1 <= size by A35, INT_1:7;
then val . (w + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . w) by A1, A34, A35, A41, NOMIN_7:10;
then D1 in dom (denaming (V,A,(val . ((len val) - k)))) by A12, A40;
then D1 in dom (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . k),(denaming (V,A,(val . ((len val) - k)))),(loc /. ((len val) - k)))) by A37, A39;
hence ((SC_Psuperpos_Seq (loc,val,p)) . m) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - m)) = ((SC_Psuperpos_Seq (loc,val,p)) . (k + 1)) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - (k + 1))) by A10, A31, A32, A12, A36, A11, NAT_1:13, NOMIN_2:35; :: thesis: verum

end;

end;

end;

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