theorem :: NOMIN_2:39

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