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