deffunc H₁( 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₁(x) from FUNCT_2:sch 4();
hence ex b₁ being UnOp of E st
for b being Point of E holds b₁ . b = (2 * a) - b ; :: thesis: verum