deffunc H_{1}( Point of E) -> Element of the carrier of E = (2 * a) - $1;

ex f being UnOp of E st

for x being Point of E holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

hence ex b_{1} being UnOp of E st

for b being Point of E holds b_{1} . b = (2 * a) - b
; :: thesis: verum

ex f being UnOp of E st

for x being Point of E holds f . x = H

hence ex b

for b being Point of E holds b