deffunc H₁( Element of G) -> Element of the carrier of G = $1 |^ b;
consider g being Function of the carrier of G, the carrier of G such that
A1: for a being Element of G holds g . a = H₁(a) from FUNCT_2:sch 4();
g is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
then reconsider g = g as Element of InnAut G by A1, Def4;
take g ; :: thesis: for a being Element of G holds g . a = a |^ b
let a be Element of G; :: thesis: g . a = a |^ b
thus g . a = a |^ b by A1; :: thesis: verum