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