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 Th56;
thus ( G is commutative implies bool G is commutative ) :: thesis: ( ( G is associative implies bool G is associative ) & ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) )

proof

assume H₁(G) is commutative ; :: according to MONOID_0:def 11 :: thesis: bool G is commutative
hence H₁( bool G) is commutative by A1, Th50; :: according to MONOID_0:def 11 :: thesis: verum

end;

thus ( G is associative implies bool G is associative ) :: thesis: ( G is uniquely-decomposable implies bool G is uniquely-decomposable )

proof

assume H₁(G) is associative ; :: according to MONOID_0:def 12 :: thesis: bool G is associative
hence H₁( bool G) is associative by A1, Th51; :: according to MONOID_0:def 12 :: thesis: verum

end;

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, Th55; :: according to MONOID_0:def 20 :: thesis: verum