deffunc H₁( Element of V) -> Element of REAL = Re (l . $1);
consider f being Function of the carrier of V,REAL such that
A1: for i being Element of V holds f . i = H₁(i) from FUNCT_2:sch 4();
addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
then reconsider f = f as Functional of (RealVS V) ;
take f ; :: thesis: for i being Element of V holds f . i = Re (l . i)
thus for i being Element of V holds f . i = Re (l . i) by A1; :: thesis: verum