let G be non empty multMagma ; :: thesis: ( G is uniquely-decomposable iff ( the multF of G is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt the multF of G holds
( a = b & b = the_unity_wrt the multF of G ) ) ) )
thus ( G is uniquely-decomposable implies ( H₂(G) is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt H₂(G) holds
( a = b & b = the_unity_wrt the multF of G ) ) ) ) :: thesis: ( the multF of G is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt the multF of G holds
( a = b & b = the_unity_wrt the multF of G ) ) implies G is uniquely-decomposable )

proof

assume A1: ( H₂(G) is having_a_unity & ( for a, b being Element of G st H₂(G) . a,b = the_unity_wrt H₂(G) holds
( a = b & b = the_unity_wrt H₂(G) ) ) ) ; :: according to MONOID_0:def 9,MONOID_0:def 20 :: thesis: ( H₂(G) is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt H₂(G) holds
( a = b & b = the_unity_wrt the multF of G ) ) )
hence H₂(G) is having_a_unity ; :: thesis: for a, b being Element of G st a * b = the_unity_wrt H₂(G) holds
( a = b & b = the_unity_wrt the multF of G )
let a, b be Element of G; :: thesis: ( a * b = the_unity_wrt H₂(G) implies ( a = b & b = the_unity_wrt the multF of G ) )
thus ( a * b = the_unity_wrt H₂(G) implies ( a = b & b = the_unity_wrt the multF of G ) ) by A1; :: thesis: verum

end;

assume A2: ( H₂(G) is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt H₂(G) holds
( a = b & b = the_unity_wrt H₂(G) ) ) ) ; :: thesis: G is uniquely-decomposable
hence H₂(G) is having_a_unity ; :: according to MONOID_0:def 9,MONOID_0:def 20 :: thesis: for a, b being Element of the carrier of G st the multF of G . a,b = the_unity_wrt the multF of G holds
( a = b & b = the_unity_wrt the multF of G )
let a, b be Element of G; :: thesis: ( the multF of G . a,b = the_unity_wrt the multF of G implies ( a = b & b = the_unity_wrt the multF of G ) )
a * b = H₂(G) . a,b ;
hence ( the multF of G . a,b = the_unity_wrt the multF of G implies ( a = b & b = the_unity_wrt the multF of G ) ) by A2; :: thesis: verum