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