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 A2: ( 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 is uniquely-decomposable
then G is unital by Def10;
then A3: ( H is unital & the_unity_wrt H₂(G) = the_unity_wrt H₂(H) ) by A1, Th32;
hence H₂(H) is having_a_unity by Def10; :: 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 Th25;
then reconsider a' = a, b' = b as Element of G by TARSKI:def 3;
H₂(H) . a,b = a * b
.= a' * b' by Th27
.= H₂(G) . a',b' ;
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 A2, A3; :: thesis: verum