deffunc H₁( Element of V) -> Element of the carrier of K = v * (f . $1);
consider F being Function of the carrier of V, the carrier of K such that
A1: for x being Element of V holds F . x = H₁(x) from FUNCT_2:sch 4();
reconsider F = F as Functional of V ;
take F ; :: thesis: for x being Element of V holds F . x = v * (f . x)
thus for x being Element of V holds F . x = v * (f . x) by A1; :: thesis: verum