deffunc H_{1}( 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_{1}(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

consider F being Function of V1,V2 such that

A1: for v being Element of V1 holds F . v = H

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