:: deftheorem Def8 defines Zero_ CSSPACE:def 10 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Zero_ (X1,X) = 0. X;