:: deftheorem defines + RUSUB_1:def 4 :
for V being RealUnitarySpace
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 } ;