set H = multMagma(# (Aut G),(AutComp G) #);

A1: ex e being Element of multMagma(# (Aut G),(AutComp G) #) st

for h being Element of multMagma(# (Aut G),(AutComp G) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

A1: ex e being Element of multMagma(# (Aut G),(AutComp G) #) st

for h being Element of multMagma(# (Aut G),(AutComp G) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

proof

for f, g, h being Element of multMagma(# (Aut G),(AutComp G) #) holds (f * g) * h = f * (g * h)
reconsider e = id the carrier of G as Element of multMagma(# (Aut G),(AutComp G) #) by Th3;

take e ; :: thesis: for h being Element of multMagma(# (Aut G),(AutComp G) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

let h be Element of multMagma(# (Aut G),(AutComp G) #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

consider A being Element of Aut G such that

A2: A = h ;

h * e = A * (id the carrier of G) by A2, Def2

.= A by FUNCT_2:17 ;

hence h * e = h by A2; :: thesis: ( e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

e * h = (id the carrier of G) * A by A2, Def2

.= A by FUNCT_2:17 ;

hence e * h = h by A2; :: thesis: ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e )

reconsider g = A " as Element of multMagma(# (Aut G),(AutComp G) #) by Th6;

take g ; :: thesis: ( h * g = e & g * h = e )

reconsider A = A as Homomorphism of G,G by Def1;

A3: A is one-to-one by Def1;

A is onto by Def1;

then A4: rng A = the carrier of G ;

thus h * g = A * (A ") by A2, Def2

.= e by A3, A4, FUNCT_2:29 ; :: thesis: g * h = e

thus g * h = (A ") * A by A2, Def2

.= e by A3, A4, FUNCT_2:29 ; :: thesis: verum

end;take e ; :: thesis: for h being Element of multMagma(# (Aut G),(AutComp G) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

let h be Element of multMagma(# (Aut G),(AutComp G) #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

consider A being Element of Aut G such that

A2: A = h ;

h * e = A * (id the carrier of G) by A2, Def2

.= A by FUNCT_2:17 ;

hence h * e = h by A2; :: thesis: ( e * h = h & ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e ) )

e * h = (id the carrier of G) * A by A2, Def2

.= A by FUNCT_2:17 ;

hence e * h = h by A2; :: thesis: ex g being Element of multMagma(# (Aut G),(AutComp G) #) st

( h * g = e & g * h = e )

reconsider g = A " as Element of multMagma(# (Aut G),(AutComp G) #) by Th6;

take g ; :: thesis: ( h * g = e & g * h = e )

reconsider A = A as Homomorphism of G,G by Def1;

A3: A is one-to-one by Def1;

A is onto by Def1;

then A4: rng A = the carrier of G ;

thus h * g = A * (A ") by A2, Def2

.= e by A3, A4, FUNCT_2:29 ; :: thesis: g * h = e

thus g * h = (A ") * A by A2, Def2

.= e by A3, A4, FUNCT_2:29 ; :: thesis: verum

proof

hence
multMagma(# (Aut G),(AutComp G) #) is strict Group
by A1, GROUP_1:def 2, GROUP_1:def 3; :: thesis: verum
let f, g, h be Element of multMagma(# (Aut G),(AutComp G) #); :: thesis: (f * g) * h = f * (g * h)

reconsider A = f, B = g, C = h as Element of Aut G ;

A5: g * h = B * C by Def2;

f * g = A * B by Def2;

hence (f * g) * h = (A * B) * C by Def2

.= A * (B * C) by RELAT_1:36

.= f * (g * h) by A5, Def2 ;

:: thesis: verum

end;reconsider A = f, B = g, C = h as Element of Aut G ;

A5: g * h = B * C by Def2;

f * g = A * B by Def2;

hence (f * g) * h = (A * B) * C by Def2

.= A * (B * C) by RELAT_1:36

.= f * (g * h) by A5, Def2 ;

:: thesis: verum