let G be strict Group; :: thesis: for f, g being Element of InnAut G holds f * g is Element of InnAut G
let f, g be Element of InnAut G; :: thesis: f * g is Element of InnAut G
A1: ( f is Element of Funcs the carrier of G,the carrier of G & g is Element of Funcs the carrier of G,the carrier of G ) by FUNCT_2:12;
A2: f * g is Element of Funcs the carrier of G,the carrier of G by FUNCT_2:12;
ex a being Element of G st
for x being Element of G holds (f * g) . x = x |^ a

proof

consider b being Element of G such that
A3: for x1 being Element of G holds f . x1 = x1 |^ b by A1, Def4;
consider c being Element of G such that
A4: for x2 being Element of G holds g . x2 = x2 |^ c by A1, Def4;
take a = c * b; :: thesis: for x being Element of G holds (f * g) . x = x |^ a
let x be Element of G; :: thesis: (f * g) . x = x |^ a
(f * g) . x = f . (g . x) by FUNCT_2:21
.= f . (x |^ c) by A4
.= (((c " ) * x) * c) |^ b by A3
.= (b " ) * ((((c " ) * x) * c) * b) by GROUP_1:def 4
.= (b " ) * (((c " ) * (x * c)) * b) by GROUP_1:def 4
.= (b " ) * ((c " ) * ((x * c) * b)) by GROUP_1:def 4
.= ((b " ) * (c " )) * ((x * c) * b) by GROUP_1:def 4
.= ((b " ) * (c " )) * (x * (c * b)) by GROUP_1:def 4
.= (((b " ) * (c " )) * x) * (c * b) by GROUP_1:def 4
.= x |^ a by GROUP_1:25 ;
hence (f * g) . x = x |^ a ; :: thesis: verum

end;

hence f * g is Element of InnAut G by A2, Def4; :: thesis: verum