for v being object
for V, A being set
for p, q being SCPartialNominativePredicate of V,A
for f, g being SCBinominativeFunction of V,A st <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))