:: deftheorem defines + CLVECT_1:def 11 :
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;