deffunc H_{1}( Element of F) -> Element of the carrier of F = - $1;

thus ex f being UnOp of the carrier of F st

for x being Element of F holds f . x = H_{1}(x)
from FUNCT_2:sch 4(); :: thesis: verum

thus ex f being UnOp of the carrier of F st

for x being Element of F holds f . x = H