let G be non empty multMagma ; 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 ; ( ( 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:
( H1( .: (G,A)) = (H1(G),H3(G)) .: A & H3( .: (G,A)) = Funcs (A,H3(G)) )
by Th17;
thus
( G is commutative implies .: (G,A) is commutative )
by A1, Th7; ( ( 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; ( ( 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; ( ( 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; ( ( 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; ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable )
assume
H1(G) is uniquely-decomposable
; MONOID_0:def 20 .: (G,A) is uniquely-decomposable
hence
H1( .: (G,A)) is uniquely-decomposable
by A1, Th14; MONOID_0:def 20 verum