let G be non empty multMagma ; :: thesis: for A being set holds

( ( G is commutative implies .: (G,A) is commutative ) & ( G is associative implies .: (G,A) is associative ) & ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

let A be set ; :: thesis: ( ( G is commutative implies .: (G,A) is commutative ) & ( G is associative implies .: (G,A) is associative ) & ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

A1: ( H_{1}( .: (G,A)) = (H_{1}(G),H_{3}(G)) .: A & H_{3}( .: (G,A)) = Funcs (A,H_{3}(G)) )
by Th17;

thus ( G is commutative implies .: (G,A) is commutative ) by A1, Th7; :: thesis: ( ( G is associative implies .: (G,A) is associative ) & ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is associative implies .: (G,A) is associative ) by A1, Th8; :: thesis: ( ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is idempotent implies .: (G,A) is idempotent ) by A1, Th11; :: thesis: ( ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is invertible implies .: (G,A) is invertible ) by A1, Th12; :: thesis: ( ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is cancelable implies .: (G,A) is cancelable ) by A1, Th13; :: thesis: ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable )

assume H_{1}(G) is uniquely-decomposable
; :: according to MONOID_0:def 20 :: thesis: .: (G,A) is uniquely-decomposable

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

( ( G is commutative implies .: (G,A) is commutative ) & ( G is associative implies .: (G,A) is associative ) & ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

let A be set ; :: thesis: ( ( G is commutative implies .: (G,A) is commutative ) & ( G is associative implies .: (G,A) is associative ) & ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

A1: ( H

thus ( G is commutative implies .: (G,A) is commutative ) by A1, Th7; :: thesis: ( ( G is associative implies .: (G,A) is associative ) & ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is associative implies .: (G,A) is associative ) by A1, Th8; :: thesis: ( ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is idempotent implies .: (G,A) is idempotent ) by A1, Th11; :: thesis: ( ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is invertible implies .: (G,A) is invertible ) by A1, Th12; :: thesis: ( ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

thus ( G is cancelable implies .: (G,A) is cancelable ) by A1, Th13; :: thesis: ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable )

assume H

hence H