:: deftheorem defines setop_SUM BHSP_5:def 2 :
for X being RealUnitarySpace
for Y being finite Subset of X holds
( ( Y <> {} implies setop_SUM (Y,X) = the addF of X ++ Y ) & ( not Y <> {} implies setop_SUM (Y,X) = 0. X ) );