let G be strict 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

hence id the carrier of G is Element of InnAut G by A1, Def4; :: thesis: verum

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

id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G)
by FUNCT_2:8;
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;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

hence id the carrier of G is Element of InnAut G by A1, Def4; :: thesis: verum