:: deftheorem Def1 defines + RUSUB_2:def 1 :
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for b₄ being strict Subspace of V holds
( b₄ = W1 + W2 iff the carrier of b₄ = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } );