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