deffunc H₁( 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₁(x) from FUNCT_2:sch 4(); :: thesis: verum