deffunc H₁( Element of V) -> Element of the carrier of R = (L1 . $1) + (L2 . $1);
consider f being Function of V,R such that
A1: for v being Element of V holds f . v = H₁(v) from FUNCT_2:sch 4();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;

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

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

end;

then reconsider f = f as Linear_Combination of V by Def2;
take f ; :: thesis: for v being Vector of V holds f . v = (L1 . v) + (L2 . v)
let v be Vector of V; :: thesis: f . v = (L1 . v) + (L2 . v)
thus f . v = (L1 . v) + (L2 . v) by A1; :: thesis: verum