deffunc H_{1}( 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_{1}(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

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

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