theorem :: NOMIN_8:19

for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A
for size being non zero Nat
for val being b₅ -element FinSequence
for p being SCPartialNominativePredicate of V,A st 3 <= size & loc,val,size are_correct_wrt d1 & local_overlapping (V,A,((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1)),((denaming (V,A,(val . (len val)))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . (size - 1))),(loc /. (len val))) in dom p & local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) in dom ((SC_Psuperpos_Seq (loc,val,p)) . (size - 1)) holds
((SC_Psuperpos_Seq (loc,val,p)) . (len (SC_Psuperpos_Seq (loc,val,p)))) . d1 = (SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,p)) . (size - 2)),(denaming (V,A,(val . 2))),(loc /. 2))) . ((LocalOverlapSeq (A,loc,val,d1,size)) . 1)