:: deftheorem defines linearly-closed VECTSP_4:def 1 :
for GF being non empty multMagma
for V being non empty ModuleStr over GF
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being Element of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Element of GF
for v being Element of V st v in V1 holds
a * v in V1 ) ) );