:: deftheorem defines SC_Psuperpos NOMIN_2:def 12 :
for V, A being set
for v being object
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds SC_Psuperpos (p,f,v) = (SCPsuperpos (V,A,v)) . (p,f);