let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H & G is uniquely-decomposable holds
H is uniquely-decomposable
let H be non empty SubStr of G; :: thesis: ( the_unity_wrt the multF of G in the carrier of H & G is uniquely-decomposable implies H is uniquely-decomposable )
assume A1: the_unity_wrt H₂(G) in H₁(H) ; :: thesis: ( not G is uniquely-decomposable or H is uniquely-decomposable )
assume that
A2: H₂(G) is having_a_unity and
A3: 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 is uniquely-decomposable
A4: G is unital by A2;
then H is unital by A1, Th30;
hence H₂(H) is having_a_unity ; :: according to MONOID_0:def 9,MONOID_0:def 20 :: thesis: for a, b being Element of the carrier of H st the multF of H . (a,b) = the_unity_wrt the multF of H holds
( a = b & b = the_unity_wrt the multF of H )
let a, b be Element of H; :: thesis: ( the multF of H . (a,b) = the_unity_wrt the multF of H implies ( a = b & b = the_unity_wrt the multF of H ) )
H₁(H) c= H₁(G) by Th23;
then reconsider a9 = a, b9 = b as Element of G ;
A5: H₂(H) . (a,b) = a * b
.= a9 * b9 by Th25
.= H₂(G) . (a9,b9) ;
the_unity_wrt H₂(G) = the_unity_wrt H₂(H) by A1, A4, Th30;
hence ( the multF of H . (a,b) = the_unity_wrt the multF of H implies ( a = b & b = the_unity_wrt the multF of H ) ) by A3, A5; :: thesis: verum