reconsider f = the carrier of V --> 0c as Element of Funcs ( the carrier of V,COMPLEX) by FUNCT_2:8;
f is C_Linear_Combination of V

proof

take {} V ; :: according to CONVEX4:def 1 :: thesis: for v being Element of V st not v in {} V holds
f . v = 0
thus for v being Element of V st not v in {} V holds
f . v = 0 by FUNCOP_1:7; :: thesis: verum

end;

then reconsider f = f as C_Linear_Combination of V ;
take f ; :: thesis: Carrier f = {}
set C = { v where v is Element of V : f . v <> 0c } ;

now :: thesis: not { v where v is Element of V : f . v <> 0c } <> {}

set x = the Element of { v where v is Element of V : f . v <> 0c } ;
assume { v where v is Element of V : f . v <> 0c } <> {} ; :: thesis: contradiction
then the Element of { v where v is Element of V : f . v <> 0c } in { v where v is Element of V : f . v <> 0c } ;
then ex v being Element of V st
( the Element of { v where v is Element of V : f . v <> 0c } = v & f . v <> 0c ) ;
hence contradiction by FUNCOP_1:7; :: thesis: verum

end;

hence Carrier f = {} ; :: thesis: verum