deffunc H₁( Element of V) -> Element of REAL = Im (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 ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider f = f as Functional of (RealVS V) ;
take f ; :: thesis: for i being Element of V holds f . i = Im (l . i)
thus for i being Element of V holds f . i = Im (l . i) by A1; :: thesis: verum