deffunc H₂( Element of V) -> Element of REAL = i * (L . $1);
consider f being Function of the carrier of V,REAL 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,REAL) by FUNCT_2:11;

now

let v be Element of V; :: thesis: ( not v in Carrier L implies f . v = 0 )
assume not v in Carrier L ; :: thesis: f . v = 0
then L . v = 0 ;
hence f . v = i * 0 by A1
.= 0 ;
:: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 5;
take f ; :: thesis: for v being VECTOR of V holds f . v = i * (L . v)
let v be VECTOR of V; :: thesis: f . v = i * (L . v)
thus f . v = i * (L . v) by A1; :: thesis: verum