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