theorem :: NOMIN_2:36

for v being object
for V, A being set
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A
for x being Element of product <*f*> st v in V & product <*f*> <> {} holds
SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)