deffunc H_{1}( Element of V) -> Element of REAL = In ((a * (L . $1)),REAL);

consider f being Function of the carrier of V,REAL such that

A1: for v being Element of V holds f . v = H_{1}(v)
from FUNCT_2:sch 4();

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

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_{1}(v)
by A1;

hence f . v = a * (L . v) ; :: thesis: verum

consider f being Function of the carrier of V,REAL such that

A1: for v being Element of V holds f . v = H

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for v being VECTOR of V st not v in Carrier L holds

f . v = 0

then reconsider f = f as Linear_Combination of V by Def3;f . v = 0

let v be VECTOR of V; :: thesis: ( not v in Carrier L implies f . v = 0 )

assume not v in Carrier L ; :: thesis: f . v = 0

then A2: L . v = 0 ;

thus f . v = H_{1}(v)
by A1

.= a * 0 by A2

.= 0 ; :: thesis: verum

end;assume not v in Carrier L ; :: thesis: f . v = 0

then A2: L . v = 0 ;

thus f . v = H

.= a * 0 by A2

.= 0 ; :: thesis: verum

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

hence f . v = a * (L . v) ; :: thesis: verum