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 size being non zero Nat
for val being b₄ -element FinSequence
for dx, dy being object
for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A
for p being SCPartialNominativePredicate of V,A
for size being non zero Nat
for val being b₃ -element FinSequence
for dx, dy being object
for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
let d1 be NonatomicND of V,A; :: thesis: for p being SCPartialNominativePredicate of V,A
for size being non zero Nat
for val being b₂ -element FinSequence
for dx, dy being object
for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
let p be SCPartialNominativePredicate of V,A; :: thesis: for size being non zero Nat
for val being b₁ -element FinSequence
for dx, dy being object
for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
let size be non zero Nat; :: thesis: for val being size -element FinSequence
for dx, dy being object
for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
let val be size -element FinSequence; :: thesis: for dx, dy being object
for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
let dx, dy be object ; :: thesis: for NN being Nat st NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p holds
((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
let NN be Nat; :: thesis: ( NN = size - 2 & loc,val,size are_correct_wrt d1 & dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) & local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p & dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) & local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p implies ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size) )
assume A1: NN = size - 2 ; :: thesis: ( not loc,val,size are_correct_wrt d1 or not dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) or not local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p or not dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) or not local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p or ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size) )
set S = SC_Psuperpos_Seq (loc,val,p);
set L = LocalOverlapSeq (A,loc,val,d1,size);
set D = denaming (V,A,(val . (len val)));
assume that
A2: loc,val,size are_correct_wrt d1 and
A3: dx = (LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1) and
A4: local_overlapping (V,A,dx,((denaming (V,A,(val . (len val)))) . dx),(loc /. (len val))) in dom p and
A5: dy = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) and
A6: local_overlapping (V,A,dy,((denaming (V,A,(val . (len val)))) . dy),(loc /. (len val))) in dom p ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)
A7: 0 + 2 <= (size - 2) + 2 by A1, XREAL_1:6;
then A8: 1 <= size by XXREAL_0:2;
reconsider N = size - 1 as Element of NAT by A7, XXREAL_0:2, INT_1:5;
A9: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by NOMIN_7:def 4;
A10: len val = size by CARD_1:def 7;
A11: (SC_Psuperpos_Seq (loc,val,p)) . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) by Def9;
A12: dom (SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val)))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . (len val)))) . d),(loc /. (len val))) in dom p & d in dom (denaming (V,A,(val . (len val)))) ) } by NOMIN_2:def 11;
A13: 2 - 1 <= N by A7, XREAL_1:9;

per cases then ( N = 1 or 1 < N ) by XXREAL_0:1;

suppose A14: N = 1 ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)

set D1 = denaming (V,A,(val . 1));
A15: (LocalOverlapSeq (A,loc,val,d1,size)) . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) by NOMIN_7:def 4;
A16: (LocalOverlapSeq (A,loc,val,d1,size)) . (N + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . N),((denaming (V,A,(val . (N + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . N)),(loc /. (N + 1))) by A9, A14, NOMIN_7:def 4;
set dd = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1));
local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) in dom (denaming (V,A,(val . (len val)))) by A2, A9, A10, A8, A15, Th15;
then local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) in dom (SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val)))) by A12, A3, A4, A14, A15;
hence ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size) by A14, A10, A15, A16, A11, NOMIN_2:35; :: thesis: verum

end;

suppose A17: 1 < N ; :: thesis: ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size)

then reconsider NN = N - 1 as Element of NAT by INT_1:5;
1 - 1 < N - 1 by A17, XREAL_1:9;
then A18: 0 + 1 <= NN by INT_1:7;
A19: N - 1 < N by XREAL_1:44;
A20: N < len (LocalOverlapSeq (A,loc,val,d1,size)) by A9, XREAL_1:44;
then NN < len (LocalOverlapSeq (A,loc,val,d1,size)) by A19, XXREAL_0:2;
then A21: (LocalOverlapSeq (A,loc,val,d1,size)) . (NN + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) by A18, NOMIN_7:def 4;
A22: (LocalOverlapSeq (A,loc,val,d1,size)) . (N + 1) = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . N),((denaming (V,A,(val . (N + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . N)),(loc /. (N + 1))) by A17, A20, NOMIN_7:def 4;
set Dn = denaming (V,A,(val . (NN + 1)));
set dd = local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1)));
local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) in dom (denaming (V,A,(val . (len val)))) by A2, A9, A10, A8, A21, A13, A20, Th15;
then local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . NN),((denaming (V,A,(val . (NN + 1)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . NN)),(loc /. (NN + 1))) in dom (SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val)))) by A1, A5, A6, A12;
hence ((SC_Psuperpos_Seq (loc,val,p)) . 1) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)) = p . ((LocalOverlapSeq (A,loc,val,d1,size)) . size) by A10, A22, A11, A21, NOMIN_2:35; :: thesis: verum

end;

end;