deffunc H_{1}( Element of V) -> Element of the carrier of GF = a * (L . $1);

consider f being Function of the carrier of V, the carrier of GF 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, the carrier of GF) by FUNCT_2:8;

take f ; :: thesis: for v being Element of V holds f . v = a * (L . v)

let v be Element of V; :: thesis: f . v = a * (L . v)

thus f . v = a * (L . v) by A1; :: thesis: verum

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

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

reconsider f = f as 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 L holds

f . v = 0. GF

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

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

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

then L . v = 0. GF ;

hence f . v = a * (0. GF) by A1

.= 0. GF ;

:: thesis: verum

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

then L . v = 0. GF ;

hence f . v = a * (0. GF) by A1

.= 0. GF ;

:: thesis: verum

take f ; :: thesis: for v being Element of V holds f . v = a * (L . v)

let v be Element of V; :: thesis: f . v = a * (L . v)

thus f . v = a * (L . v) by A1; :: thesis: verum