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: g is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
A2: f is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
A3: ex a being Element of G st
for x being Element of G holds (f * g) . x = x |^ a
proof
consider c being Element of G such that
A4: for x2 being Element of G holds g . x2 = x2 |^ c by A1, Def4;
consider b being Element of G such that
A5: for x1 being Element of G holds f . x1 = x1 |^ b by A2, 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:15
.= f . (x |^ c) by A4
.= (((c ") * x) * c) |^ b by A5
.= (b ") * ((((c ") * x) * c) * b) by GROUP_1:def 3
.= (b ") * (((c ") * (x * c)) * b) by GROUP_1:def 3
.= (b ") * ((c ") * ((x * c) * b)) by GROUP_1:def 3
.= ((b ") * (c ")) * ((x * c) * b) by GROUP_1:def 3
.= ((b ") * (c ")) * (x * (c * b)) by GROUP_1:def 3
.= (((b ") * (c ")) * x) * (c * b) by GROUP_1:def 3
.= x |^ a by GROUP_1:17 ;
hence (f * g) . x = x |^ a ; :: thesis: verum
end;
f * g is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
hence f * g is Element of InnAut G by A3, Def4; :: thesis: verum