set SO = the Sorts of U1;

set H = multMagma(# (MSAAut U1),(MSAAutComp U1) #);

A1: ex e being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

set H = multMagma(# (MSAAut U1),(MSAAutComp U1) #);

A1: ex e being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

proof

for f, g, h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds (f * g) * h = f * (g * h)
reconsider e = id the Sorts of U1 as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th24;

take e ; :: thesis: for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

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

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

consider A being Element of MSAAut U1 such that

A2: A = h ;

h * e = (id the Sorts of U1) ** A by A2, Def6

.= A by MSUALG_3:4 ;

hence h * e = h by A2; :: thesis: ( e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

e * h = A ** (id the Sorts of U1) by A2, Def6

.= A by MSUALG_3:3 ;

hence e * h = h by A2; :: thesis: ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

reconsider g = A "" as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th25;

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

A3: ( A is "onto" & A is "1-1" ) by Lm3;

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

.= e by A3, MSUALG_3:5 ; :: thesis: g * h = e

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

.= e by A3, MSUALG_3:5 ; :: thesis: verum

end;take e ; :: thesis: for h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

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

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

consider A being Element of MSAAut U1 such that

A2: A = h ;

h * e = (id the Sorts of U1) ** A by A2, Def6

.= A by MSUALG_3:4 ;

hence h * e = h by A2; :: thesis: ( e * h = h & ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

e * h = A ** (id the Sorts of U1) by A2, Def6

.= A by MSUALG_3:3 ;

hence e * h = h by A2; :: thesis: ex g being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) st

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

reconsider g = A "" as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th25;

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

A3: ( A is "onto" & A is "1-1" ) by Lm3;

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

.= e by A3, MSUALG_3:5 ; :: thesis: g * h = e

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

.= e by A3, MSUALG_3:5 ; :: thesis: verum

proof

hence
multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group
by A1, GROUP_1:def 2, GROUP_1:def 3; :: thesis: verum
let f, g, h be Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #); :: thesis: (f * g) * h = f * (g * h)

reconsider A = f, B = g, C = h as Element of MSAAut U1 ;

A4: g * h = C ** B by Def6;

f * g = B ** A by Def6;

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

.= (C ** B) ** A by PBOOLE:140

.= f * (g * h) by A4, Def6 ;

:: thesis: verum

end;reconsider A = f, B = g, C = h as Element of MSAAut U1 ;

A4: g * h = C ** B by Def6;

f * g = B ** A by Def6;

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

.= (C ** B) ** A by PBOOLE:140

.= f * (g * h) by A4, Def6 ;

:: thesis: verum