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₁( .: G,A) = H₁(G),H₃(G) .: A & H₃( .: G,A) = Funcs A,H₃(G) ) by Th18;
thus ( G is commutative implies .: G,A is commutative ) :: 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 ) )

proof

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

end;

thus ( G is associative implies .: G,A is associative ) :: 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 ) )

proof

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

end;

thus ( G is idempotent implies .: G,A is idempotent ) :: 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 ) )

proof

assume H₁(G) is idempotent ; :: according to MONOID_0:def 13 :: thesis: .: G,A is idempotent
hence H₁( .: G,A) is idempotent by A1, Th12; :: according to MONOID_0:def 13 :: thesis: verum

end;

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

proof

assume H₁(G) is invertible ; :: according to MONOID_0:def 16 :: thesis: .: G,A is invertible
hence H₁( .: G,A) is invertible by A1, Th13; :: according to MONOID_0:def 16 :: thesis: verum

end;

thus ( G is cancelable implies .: G,A is cancelable ) :: thesis: ( G is uniquely-decomposable implies .: G,A is uniquely-decomposable )

proof

assume H₁(G) is cancelable ; :: according to MONOID_0:def 19 :: thesis: .: G,A is cancelable
hence H₁( .: G,A) is cancelable by A1, Th14; :: according to MONOID_0:def 19 :: thesis: verum

end;

assume H₁(G) is uniquely-decomposable ; :: according to MONOID_0:def 20 :: thesis: .: G,A is uniquely-decomposable
hence H₁( .: G,A) is uniquely-decomposable by A1, Th15; :: according to MONOID_0:def 20 :: thesis: verum