set f = L1 + L2;
A1: ( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:def 1;
A5: 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 A4: L1 + L2 is Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;

now

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

end;

hence L1 + L2 is Linear_Combination of V by A4, Def4; :: thesis: verum