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