:: deftheorem defines setop_xPROD BHSP_5:def 7 :
for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X holds
( ( Y <> {} implies setop_xPROD (x,Y,X) = setop_xPre_PROD (x,Y,X) ) & ( not Y <> {} implies setop_xPROD (x,Y,X) = 0 ) );