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 ) )
proof
reconsider e =
id the
Sorts of
U1 as
Element of
multMagma(#
(MSAAut U1),
(MSAAutComp U1) #)
by Th24;
take
e
;
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) #);
( 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;
( 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;
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
;
( 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
;
g * h = e
thus g * h =
A ** (A "")
by A2, Def6
.=
e
by A3, MSUALG_3:5
;
verum
end;
for f, g, h being Element of multMagma(# (MSAAut U1),(MSAAutComp U1) #) holds (f * g) * h = f * (g * h)
hence
multMagma(# (MSAAut U1),(MSAAutComp U1) #) is Group
by A1, GROUP_1:def 2, GROUP_1:def 3; verum