:: deftheorem Def10 defines SC_Psuperpos NOMIN_2:def 10 :
for V, A being set
for p being SCPartialNominativePredicate of V,A
for g being b₁,b₂ -FPrg-yielding FinSequence st product g <> {} holds
for X being Function
for x being Element of product g holds SC_Psuperpos (p,x,X) = (SCPsuperpos (g,X)) . (p,x);