:: deftheorem defines linearly-closed CLVECT_1:def 7 :
for V being ComplexLinearSpace
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1 ) ) );