let G be non empty multMagma ; :: thesis: ( G is associative implies ( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) ) )
assume A1: G is associative ; :: thesis: ( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) )
thus ( G is invertible implies ( G is unital & H2(G) is having_an_inverseOp ) ) :: thesis: ( G is unital & the multF of G is having_an_inverseOp implies G is invertible )
proof
consider e being Element of G;
assume A2: G is invertible ; :: thesis: ( G is unital & H2(G) is having_an_inverseOp )
then consider x, y being Element of G such that
A3: e * x = e and
A4: y * e = e by Th12;
A5: now
let a be Element of G; :: thesis: ( y * a = a & a * x = a )
A6: ex b, c being Element of G st
( e * b = a & c * e = a ) by A2, Th12;
hence y * a = a by A1, A4, Lm2; :: thesis: a * x = a
thus a * x = a by A1, A3, A6, Lm2; :: thesis: verum
end;
then A7: ( y * x = x & y * x = y ) ;
hence G is unital by A5, Th6; :: thesis: H2(G) is having_an_inverseOp
defpred S1[ Element of G, Element of G] means ( $1 * $2 = x & $2 * $1 = x );
A8: for a being Element of G ex b being Element of G st S1[a,b]
proof
let a be Element of G; :: thesis: ex b being Element of G st S1[a,b]
consider b, c being Element of G such that
A9: ( a * b = x & c * a = x ) by A2, Th12;
take b ; :: thesis: S1[a,b]
( c * (a * b) = (c * a) * b & x * b = b ) by A1, A5, A7, Lm2;
hence S1[a,b] by A5, A9; :: thesis: verum
end;
ex f being Function of the carrier of G,the carrier of G st
for x being Element of G holds S1[x,f . x] from FUNCT_2:sch 3(A8);
 then consider u being UnOp of H1(G) such that
A10: for a being Element of G holds S1[a,u . a] ;
now
let b be Element of G; :: thesis: ( H2(G) . x,b = b & H2(G) . b,x = b )
( x * b = H2(G) . x,b & b * x = H2(G) . b,x ) ;
hence ( H2(G) . x,b = b & H2(G) . b,x = b ) by A5, A7; :: thesis: verum
end;
then x is_a_unity_wrt H2(G) by BINOP_1:11;
then A11: x = the_unity_wrt H2(G) by BINOP_1:def 8;
take u ; :: according to FINSEQOP:def 2 :: thesis: u is_an_inverseOp_wrt H2(G)
let a be Element of G; :: according to FINSEQOP:def 1 :: thesis: ( H2(G) . a,(u . a) = the_unity_wrt H2(G) & H2(G) . (u . a),a = the_unity_wrt H2(G) )
( H2(G) . a,(u . a) = a * (u . a) & H2(G) . (u . a),a = (u . a) * a ) ;
hence ( H2(G) . a,(u . a) = the_unity_wrt H2(G) & H2(G) . (u . a),a = the_unity_wrt H2(G) ) by A10, A11; :: thesis: verum
end;
assume A12: H2(G) is having_a_unity ; :: according to MONOID_0:def 10 :: thesis: ( not the multF of G is having_an_inverseOp or G is invertible )
given u being UnOp of H1(G) such that A13: u is_an_inverseOp_wrt H2(G) ; :: according to FINSEQOP:def 2 :: thesis: G is invertible
let a be Element of G; :: according to MONOID_0:def 5,MONOID_0:def 16 :: thesis: for b being Element of the carrier of G ex r, l being Element of the carrier of G st
( the multF of G . a,r = b & the multF of G . l,a = b )
let c be Element of G; :: thesis: ex r, l being Element of the carrier of G st
( the multF of G . a,r = c & the multF of G . l,a = c )
take l = (u . a) * c; :: thesis: ex l being Element of the carrier of G st
( the multF of G . a,l = c & the multF of G . l,a = c )
take r = c * (u . a); :: thesis: ( the multF of G . a,l = c & the multF of G . r,a = c )
thus H2(G) . a,l = a * l
.= (a * (u . a)) * c by A1, Lm2
.= H2(G) . (the_unity_wrt H2(G)),c by A13, FINSEQOP:def 1
.= c by A12, SETWISEO:23 ; :: thesis: the multF of G . r,a = c
thus H2(G) . r,a = r * a
.= c * ((u . a) * a) by A1, Lm2
.= H2(G) . c,(the_unity_wrt H2(G)) by A13, FINSEQOP:def 1
.= c by A12, SETWISEO:23 ; :: thesis: verum