let G be non empty multMagma ; :: thesis: ( ( G is commutative implies bool G is commutative ) & ( G is associative implies bool G is associative ) & ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) )
A1: ( H₁( bool G) = H₁(G) .:^2 & H₃( bool G) = bool H₃(G) ) by Th55;
thus ( G is commutative implies bool G is commutative ) by A1, Th49; :: thesis: ( ( G is associative implies bool G is associative ) & ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) )
thus ( G is associative implies bool G is associative ) by A1, Th50; :: thesis: ( G is uniquely-decomposable implies bool G is uniquely-decomposable )
assume H₁(G) is uniquely-decomposable ; :: according to MONOID_0:def 20 :: thesis: bool G is uniquely-decomposable
hence H₁( bool G) is uniquely-decomposable by A1, Th54; :: according to MONOID_0:def 20 :: thesis: verum