let G be non empty multMagma ; :: thesis: ( G is associative & G is invertible implies G is Group-like )
assume A1: ( G is associative & G is invertible ) ; :: thesis: G is Group-like
then G is unital by Th15;
then consider a being Element of G such that
A2: for b being Element of G holds
( a * b = b & b * a = b ) ;
take a ; :: according to GROUP_1:def 2 :: thesis: for b₁ being Element of the carrier of G holds
( b₁ [*] a = b₁ & a [*] b₁ = b₁ & ex b₂ being Element of the carrier of G st
( b₁ [*] b₂ = a & b₂ [*] b₁ = a ) )
let b be Element of G; :: thesis: ( b [*] a = b & a [*] b = b & ex b₁ being Element of the carrier of G st
( b [*] b₁ = a & b₁ [*] b = a ) )
thus ( b * a = b & a * b = b ) by A2; :: thesis: ex b₁ being Element of the carrier of G st
( b [*] b₁ = a & b₁ [*] b = a )
H₂(G) is invertible by A1;
then consider l, r being Element of G such that
A3: ( H₂(G) . (b,l) = a & H₂(G) . (r,b) = a ) ;
take l ; :: thesis: ( b [*] l = a & l [*] b = a )
A4: ( b * l = a & r * b = a ) by A3;
r = r * a by A2
.= a * l by A1, A4
.= l by A2 ;
hence ( b [*] l = a & l [*] b = a ) by A3; :: thesis: verum