theorem :: CLVECT_1:63

for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm5;