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