set H = multMagma(# (UAAut UA),() #);
A1: ex e being Element of multMagma(# (UAAut UA),() #) st
for h being Element of multMagma(# (UAAut UA),() #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),() #) st
( h * g = e & g * h = e ) )
proof
reconsider e = id the carrier of UA as Element of multMagma(# (UAAut UA),() #) by Th3;
take e ; :: thesis: for h being Element of multMagma(# (UAAut UA),() #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (UAAut UA),() #) st
( h * g = e & g * h = e ) )

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

consider A being Element of UAAut UA such that
A2: A = h ;
h * e = (id the carrier of UA) * A by
.= A by FUNCT_2:17 ;
hence h * e = h by A2; :: thesis: ( e * h = h & ex g being Element of multMagma(# (UAAut UA),() #) st
( h * g = e & g * h = e ) )

e * h = A * (id the carrier of UA) by
.= A by FUNCT_2:17 ;
hence e * h = h by A2; :: thesis: ex g being Element of multMagma(# (UAAut UA),() #) st
( h * g = e & g * h = e )

reconsider g = A " as Element of multMagma(# (UAAut UA),() #) by Th5;
take g ; :: thesis: ( h * g = e & g * h = e )
A3: A is_isomorphism by Def1;
then A4: A is one-to-one by ALG_1:7;
A is_epimorphism by A3;
then A5: rng A = the carrier of UA ;
thus h * g = (A ") * A by
.= e by ; :: thesis: g * h = e
thus g * h = A * (A ") by
.= e by ; :: thesis: verum
end;
for f, g, h being Element of multMagma(# (UAAut UA),() #) holds (f * g) * h = f * (g * h)
proof
let f, g, h be Element of multMagma(# (UAAut UA),() #); :: thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of UAAut UA ;
A6: g * h = C * B by Def2;
f * g = B * A by Def2;
hence (f * g) * h = C * (B * A) by Def2
.= (C * B) * A by RELAT_1:36
.= f * (g * h) by ;
:: thesis: verum
end;
hence multMagma(# (UAAut UA),() #) is Group by ; :: thesis: verum