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