let M be non empty well-unital uniquely-decomposable multLoopStr ; :: thesis: for N being non empty MonoidalSubStr of M holds N is uniquely-decomposable
let N be non empty MonoidalSubStr of M; :: thesis: N is uniquely-decomposable
( N is SubStr of M & H₃(M) = the_unity_wrt H₂(M) & H₃(M) = H₃(N) ) by Def25, Th19, Th23;
hence N is uniquely-decomposable by Th38; :: thesis: verum