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