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