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