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 & H₂(G) is having_an_inverseOp ) ) :: thesis: ( G is unital & the multF of G is having_an_inverseOp implies G is invertible )

proof

assume A2: G is invertible ; :: thesis: ( G is unital & H₂(G) is having_an_inverseOp )
consider e being Element of G;
consider x, y being Element of G such that
A3: ( e * x = e & y * e = e ) by A2, Th12;

A4: now

let a be Element of G; :: thesis: ( y * a = a & a * x = a )
consider b, c being Element of G such that
A5: ( e * b = a & c * e = a ) by A2, Th12;
thus y * a = a by A1, A3, A5, Lm2; :: thesis: a * x = a
thus a * x = a by A1, A3, A5, Lm2; :: thesis: verum

end;

then A6: ( y * x = x & y * x = y ) ;
hence G is unital by A4, Th6; :: thesis: H₂(G) is having_an_inverseOp
defpred S₁[ Element of G, Element of G] means ( $1 * $2 = x & $2 * $1 = x );
A7: for a being Element of G ex b being Element of G st S₁[a,b]

proof

let a be Element of G; :: thesis: ex b being Element of G st S₁[a,b]
consider b, c being Element of G such that
A8: ( a * b = x & c * a = x ) by A2, Th12;
take b ; :: thesis: S₁[a,b]
( c * (a * b) = (c * a) * b & x * b = b & c * x = c ) by A1, A4, A6, Lm2;
hence S₁[a,b] by A8; :: thesis: verum

end;

ex f being Function of the carrier of G,the carrier of G st
for x being Element of G holds S₁[x,f . x] from FUNCT_2:sch 3(A7);
then consider u being UnOp of H₁(G) such that
A9: for a being Element of G holds S₁[a,u . a] ;
take u ; :: according to FINSEQOP:def 2 :: thesis: u is_an_inverseOp_wrt H₂(G)
let a be Element of G; :: according to FINSEQOP:def 1 :: thesis: ( H₂(G) . a,(u . a) = the_unity_wrt H₂(G) & H₂(G) . (u . a),a = the_unity_wrt H₂(G) )

now

let b be Element of G; :: thesis: ( H₂(G) . x,b = b & H₂(G) . b,x = b )
( x * b = H₂(G) . x,b & b * x = H₂(G) . b,x ) ;
hence ( H₂(G) . x,b = b & H₂(G) . b,x = b ) by A4, A6; :: thesis: verum

end;

then x is_a_unity_wrt H₂(G) by BINOP_1:11;
then ( x = the_unity_wrt H₂(G) & H₂(G) . a,(u . a) = a * (u . a) & H₂(G) . (u . a),a = (u . a) * a ) by BINOP_1:def 8;
hence ( H₂(G) . a,(u . a) = the_unity_wrt H₂(G) & H₂(G) . (u . a),a = the_unity_wrt H₂(G) ) by A9; :: thesis: verum

end;

assume A10: H₂(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 H₁(G) such that A11: u is_an_inverseOp_wrt H₂(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 H₂(G) . a,l = a * l
.= (a * (u . a)) * c by A1, Lm2
.= H₂(G) . (the_unity_wrt H₂(G)),c by A11, FINSEQOP:def 1
.= c by A10, SETWISEO:23 ; :: thesis: the multF of G . r,a = c
thus H₂(G) . r,a = r * a
.= c * ((u . a) * a) by A1, Lm2
.= H₂(G) . c,(the_unity_wrt H₂(G)) by A11, FINSEQOP:def 1
.= c by A10, SETWISEO:23 ; :: thesis: verum