theorem :: NOMIN_3:31

for V, A being set
for p being SCPartialNominativePredicate of V,A
for E being b₁,b₂ -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} holds
<*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))