deffunc H₁( Element of G) -> Element of the carrier of G = a + $1;
consider f being Function of the carrier of G, the carrier of G such that
A1: 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 = a + x
thus for x being Element of G holds f . x = a + x by A1; :: thesis: verum