let N be multLoopStr ; :: thesis: ( N is MonoidalSubStr of M iff ( the multF of N c= the multF of M & 1. N = 1. M ) )
thus ( N is MonoidalSubStr of M implies ( H₂(N) c= H₂(M) & H₃(N) = H₃(M) ) ) :: thesis: ( the multF of N c= the multF of M & 1. N = 1. M implies N is MonoidalSubStr of M )

proof

assume ( H₂(N) c= H₂(M) & ( for K being multLoopStr st M = K holds
H₃(N) = H₃(K) ) ) ; :: according to MONOID_0:def 24 :: thesis: ( H₂(N) c= H₂(M) & H₃(N) = H₃(M) )
hence ( H₂(N) c= H₂(M) & H₃(N) = H₃(M) ) ; :: thesis: verum

end;

assume ( H₂(N) c= H₂(M) & H₃(N) = H₃(M) ) ; :: thesis: N is MonoidalSubStr of M
hence ( H₂(N) c= H₂(M) & ( for K being multLoopStr st M = K holds
H₃(N) = H₃(K) ) ) ; :: according to MONOID_0:def 24 :: thesis: verum