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

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

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

f * g is Element of Funcs ( the carrier of G, the carrier of G)
by FUNCT_2:9;
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;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

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