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
A1: H₃(M) = H₃(N) by Def25;
( N is SubStr of M & H₃(M) = the_unity_wrt H₂(M) ) by Th17, Th21;
hence N is uniquely-decomposable by A1, Th36; :: thesis: verum