reconsider f = L1 + L2 as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for v being Element of V st not v in (Carrier L1) \/ (Carrier L2) holds
f . v = 0

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

end;

hence L1 + L2 is Linear_Combination of V by Def3; :: thesis: verum