theorem Th41: :: CLVECT_1:41
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V st v in W holds
- v in W