set f = L1 + L2;
A1: ( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:def 1;
A2: dom (L1 + L2) = (dom L1) /\ (dom L2) by VFUNCT_1:def 1;
then L1 + L2 is Function of V,GF by A1, FUNCT_2:67;
then A3: L1 + L2 is Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

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

let v be Element of V; :: thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies (L1 + L2) . v = 0. GF )
assume A4: not v in (Carrier L1) \/ (Carrier L2) ; :: thesis: (L1 + L2) . v = 0. GF
then not v in Carrier L2 by XBOOLE_0:def 3;
then A5: L2 . v = 0. GF ;
A6: ( L1 /. v = L1 . v & L2 /. v = L2 . v ) by A1, PARTFUN1:def 6;
not v in Carrier L1 by A4, XBOOLE_0:def 3;
then A7: L1 . v = 0. GF ;
thus (L1 + L2) . v = (L1 + L2) /. v by A1, A2, PARTFUN1:def 6
.= (0. GF) + (0. GF) by A1, A2, A5, A6, A7, VFUNCT_1:def 1
.= 0. GF by RLVECT_1:4 ; :: thesis: verum

end;

hence L1 + L2 is Linear_Combination of V by A3, Def1; :: thesis: verum