set H = multMagma(# (UAAut UA),(UAAutComp UA) #);
( multMagma(# (UAAut UA),(UAAutComp UA) #) is associative & multMagma(# (UAAut UA),(UAAutComp UA) #) is Group-like )

proof

thus for f, g, h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds (f * g) * h = f * (g * h) :: according to GROUP_1:def 4 :: thesis: multMagma(# (UAAut UA),(UAAutComp UA) #) is Group-like

proof

let f, g, h be Element of multMagma(# (UAAut UA),(UAAutComp UA) #); :: thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of UAAut UA ;
A1: f * g = B * A by Def2;
A2: g * h = C * B by Def2;
thus (f * g) * h = C * (B * A) by A1, Def2
.= (C * B) * A by RELAT_1:55
.= f * (g * h) by A2, Def2 ; :: thesis: verum

end;

thus ex e being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
for h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) ) :: according to GROUP_1:def 3 :: thesis: verum

proof

reconsider e = id the carrier of UA as Element of multMagma(# (UAAut UA),(UAAutComp UA) #) by Th4;
take e ; :: thesis: for h being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# (UAAut UA),(UAAutComp UA) #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) )
consider A being Element of UAAut UA such that
A3: A = h ;
h * e = (id the carrier of UA) * A by A3, Def2
.= A by FUNCT_2:23 ;
hence h * e = h by A3; :: thesis: ( e * h = h & ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e ) )
e * h = A * (id the carrier of UA) by A3, Def2
.= A by FUNCT_2:23 ;
hence e * h = h by A3; :: thesis: ex g being Element of multMagma(# (UAAut UA),(UAAutComp UA) #) st
( h * g = e & g * h = e )
reconsider g = A " as Element of multMagma(# (UAAut UA),(UAAutComp UA) #) by Th6;
take g ; :: thesis: ( h * g = e & g * h = e )
A4: A is_isomorphism UA,UA by Def1;
then A5: A is one-to-one by ALG_1:8;
A is_epimorphism UA,UA by A4, ALG_1:def 4;
then A6: rng A = the carrier of UA by ALG_1:def 3;
thus h * g = (A " ) * A by A3, Def2
.= e by A5, A6, FUNCT_2:35 ; :: thesis: g * h = e
thus g * h = A * (A " ) by A3, Def2
.= e by A5, A6, FUNCT_2:35 ; :: thesis: verum

end;

end;

hence multMagma(# (UAAut UA),(UAAutComp UA) #) is Group ; :: thesis: verum