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