theorem :: NOMIN_3:33

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