deffunc H₁( Element of G) -> Element of G = - $1;
consider u being UnOp of G such that
A1: for h being Element of G holds u . h = H₁(h) from FUNCT_2:sch 4();
take u ; :: thesis: for h being Element of G holds u . h = - h
let h be Element of G; :: thesis: u . h = - h
thus u . h = - h by A1; :: thesis: verum