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: H₃(M) is_a_unity_wrt H₂(M) by Def21;
A2: ( N is SubStr of M & H₃(N) = H₃(M) ) by Def24, Th23;

now

let a be Element of N; :: thesis: ( H₂(N) . H₃(N),a = a & H₂(N) . a,H₃(N) = a )
H₁(N) c= H₁(M) by Th25;
then reconsider a9 = a as Element of M by TARSKI:def 3;
thus H₂(N) . H₃(N),a = H₃(N) * a
.= H₃(M) * a9 by A2, Th27
.= a by A1, BINOP_1:11 ; :: thesis: H₂(N) . a,H₃(N) = a
thus H₂(N) . a,H₃(N) = a * H₃(N)
.= a9 * H₃(M) by A2, Th27
.= a by A1, BINOP_1:11 ; :: thesis: verum

end;

hence H₃(N) is_a_unity_wrt H₂(N) by BINOP_1:11; :: according to MONOID_0:def 21 :: thesis: verum