reconsider f = L1 + L2 as Element of Funcs the carrier of V,COMPLEX by FUNCT_2:11;

now

let v be Element of V; :: thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies f . v = 0 )
assume not v in (Carrier L1) \/ (Carrier L2) ; :: thesis: f . v = 0
then ( not v in Carrier L1 & not v in Carrier L2 ) by XBOOLE_0:def 3;
then ( L1 . v = 0 & L2 . v = 0 ) ;
hence f . v = 0 + 0 by VALUED_1:1
.= 0 ;
:: thesis: verum

end;

hence L1 + L2 is C_Linear_Combination of V by Def1; :: thesis: verum