reconsider W = [#] V as non empty Subset of V ;
( W is add-closed & W is having-inverse & ( for a being Complex
for v being Element of V st v in W holds
a * v in W ) ) ;
then A1: W is Cadditively-linearly-closed by Def2;
( 1. V in W & ( for v, u being Element of V st v in W & u in W holds
v * u in W ) ) ;
then W is multiplicatively-closed by C0SP1:def 4;
hence ex b₁ being non empty Subset of V st
( b₁ is Cadditively-linearly-closed & b₁ is multiplicatively-closed ) by A1; :: thesis: verum