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_{1}( bool G) = H_{1}(G) .:^2 & H_{3}( bool G) = bool H_{3}(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_{1}(G) is uniquely-decomposable
; :: according to MONOID_0:def 20 :: thesis: bool G is uniquely-decomposable

hence H_{1}( bool G) is uniquely-decomposable
by A1, Th54; :: according to MONOID_0:def 20 :: thesis: verum

A1: ( H

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

hence H