deffunc H₁( Element of V) -> Element of INT = In ((a * (L . $1)),INT);
consider f being Function of the carrier of V,INT 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,INT) by FUNCT_2:8;

now :: thesis: for v being VECTOR of V st not v in Carrier L holds
f . v = 0

let v be VECTOR of V; :: thesis: ( not v in Carrier L implies f . v = 0 )
reconsider N0 = 0 as Element of INT by INT_1:def 2;
assume not v in Carrier L ; :: thesis: f . v = 0
then A2: L . v = N0 ;
thus f . v = H₁(v) by A1
.= 0 by A2 ; :: thesis: verum

end;

then reconsider f = f as Z_Linear_Combination of V by Def18;
take f ; :: thesis: for v being VECTOR of V holds f . v = a * (L . v)
let v be VECTOR of V; :: thesis: f . v = a * (L . v)
f . v = H₁(v) by A1;
hence f . v = a * (L . v) ; :: thesis: verum