deffunc H_{5}( 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_{5}(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

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

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