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 ( H2(G) is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt H2(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: H2(G) is having_a_unity and
A2: for a, b being Element of G st H2(G) . (a,b) = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt H2(G) ) ; :: according to MONOID_0:def 9,MONOID_0:def 20 :: thesis: ( H2(G) is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt the multF of G ) ) )
thus H2(G) is having_a_unity by A1; :: thesis: for a, b being Element of G st a * b = the_unity_wrt H2(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 H2(G) implies ( a = b & b = the_unity_wrt the multF of G ) )
thus ( a * b = the_unity_wrt H2(G) implies ( a = b & b = the_unity_wrt the multF of G ) ) by A2; :: thesis: verum
end;
assume that
A3: H2(G) is having_a_unity and
A4: for a, b being Element of G st a * b = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt H2(G) ) ; :: thesis: G is uniquely-decomposable
thus H2(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 = H2(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