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 ( H2(N) c= H2(M) & H3(N) = H3(M) ) ) :: thesis: ( the multF of N c= the multF of M & 1. N = 1. M implies N is MonoidalSubStr of M )
proof
assume ( H2(N) c= H2(M) & ( for K being multLoopStr st M = K holds
H3(N) = H3(K) ) ) ; :: according to MONOID_0:def 24 :: thesis: ( H2(N) c= H2(M) & H3(N) = H3(M) )
hence ( H2(N) c= H2(M) & H3(N) = H3(M) ) ; :: thesis: verum
end;
assume ( H2(N) c= H2(M) & H3(N) = H3(M) ) ; :: thesis: N is MonoidalSubStr of M
hence ( H2(N) c= H2(M) & ( for K being multLoopStr st M = K holds
H3(N) = H3(K) ) ) ; :: according to MONOID_0:def 24 :: thesis: verum