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

hence
L1 + L2 is Linear_Combination of V
by Def3; :: thesis: verumf . 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;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