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;

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

hence
L1 + L2 is Linear_Combination of V
by A3, Def1; :: thesis: verum(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;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