let M be non empty well-unital multLoopStr ; :: thesis: for N being non empty MonoidalSubStr of M holds N is well-unital
let N be non empty MonoidalSubStr of M; :: thesis: N is well-unital
A1:
N is SubStr of M
by Th23;
A2:
( H3(N) = H3(M) & H3(M) is_a_unity_wrt H2(M) )
by Def21, Def24;
now let a be
Element of
N;
:: thesis: ( H2(N) . H3(N),a = a & H2(N) . a,H3(N) = a )
H1(
N)
c= H1(
M)
by Th25;
then reconsider a' =
a as
Element of
M by TARSKI:def 3;
thus H2(
N)
. H3(
N),
a =
H3(
N)
* a
.=
H3(
M)
* a'
by A1, A2, Th27
.=
a
by A2, BINOP_1:11
;
:: thesis: H2(N) . a,H3(N) = athus H2(
N)
. a,
H3(
N) =
a * H3(
N)
.=
a' * H3(
M)
by A1, A2, Th27
.=
a
by A2, BINOP_1:11
;
:: thesis: verum end;
hence
H3(N) is_a_unity_wrt H2(N)
by BINOP_1:11; :: according to MONOID_0:def 21 :: thesis: verum