let G be Group; :: thesis: id the carrier of G is Element of InnAut G
set I = id the carrier of G;
A1: ex a being Element of G st
for x being Element of G holds (id the carrier of G) . x = x |^ a

proof

take a = 1_ G; :: thesis: for x being Element of G holds (id the carrier of G) . x = x |^ a
let x be Element of G; :: thesis: (id the carrier of G) . x = x |^ a
A2: a " = 1_ G by GROUP_1:8;
thus (id the carrier of G) . x = x
.= x * a by GROUP_1:def 4
.= x |^ a by A2, GROUP_1:def 4 ; :: thesis: verum

end;

id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
hence id the carrier of G is Element of InnAut G by A1, Def4; :: thesis: verum