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