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 that
A1: H₂(G) is having_a_unity and
A2: 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 ) ) )
thus H₂(G) is having_a_unity by A1; :: 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 A2; :: thesis: verum

end;

assume that
A3: H₂(G) is having_a_unity and
A4: 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
thus H₂(G) is having_a_unity by A3; :: 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 A4; :: thesis: verum