set H = multMagma(# (MSAAut U1),(MSAAutComp U1) #);
set SO = the Sorts of U1;
( multMagma(# (MSAAut U1),(MSAAutComp U1) #) is associative & multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group-like )

proof

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

proof

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 ;
A1: f * g = B ** A by Def8;
A2: g * h = C ** B by Def8;
thus (f * g) * h = C ** (B ** A) by A1, Def8
.= (C ** B) ** A by PBOOLE:154
.= f * (g * h) by A2, Def8 ; :: thesis: verum

end;

thus 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 ) ) :: according to GROUP_1:def 3 :: thesis: verum

proof

reconsider e = id the Sorts of U1 as Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) by Th31;
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
A3: A = h ;
A4: ( A is "onto" & A is "1-1" ) by Lm3;
h * e = (id the Sorts of U1) ** A by A3, Def8
.= A by MSUALG_3:4 ;
hence h * e = h by A3; :: 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 A3, Def8
.= A by MSUALG_3:3 ;
hence e * h = h by A3; :: 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 Th32;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = (A "" ) ** A by A3, Def8
.= e by A4, MSUALG_3:5 ; :: thesis: g * h = e
thus g * h = A ** (A "" ) by A3, Def8
.= e by A4, MSUALG_3:5 ; :: thesis: verum

end;

end;

hence multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group ; :: thesis: verum