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