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;