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, Th21;

now :: thesis: for a being Element of N holds
( H₂(N) . (H₃(N),a) = a & H₂(N) . (a,H₃(N)) = a )

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 Th23;
then reconsider a9 = a as Element of M ;
thus H₂(N) . (H₃(N),a) = H₃(N) * a
.= H₃(M) * a9 by A2, Th25
.= a by A1, BINOP_1:3 ; :: thesis: H₂(N) . (a,H₃(N)) = a
thus H₂(N) . (a,H₃(N)) = a * H₃(N)
.= a9 * H₃(M) by A2, Th25
.= a by A1, BINOP_1:3 ; :: thesis: verum

end;

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