let G be non empty multMagma ; :: thesis: for M being non empty multLoopStr holds
( G is SubStr of G & M is MonoidalSubStr of M )
let M be non empty multLoopStr ; :: thesis: ( G is SubStr of G & M is MonoidalSubStr of M )
thus H₂(G) c= H₂(G) ; :: according to MONOID_0:def 23 :: thesis: M is MonoidalSubStr of M
thus H₂(M) c= H₂(M) ; :: according to MONOID_0:def 25 :: thesis: 1. M = 1. M
thus 1. M = 1. M ; :: thesis: verum