:: deftheorem Def9 defines (0). CLVECT_1:def 9 :
for V being ComplexLinearSpace
for b₂ being strict Subspace of V holds
( b₂ = (0). V iff the carrier of b₂ = {(0. V)} );