deffunc H4( Element of D * , Element of D * ) -> Element of D * = $1 ^ $2;
consider f being BinOp of (D *) such that
A1:
for a, b being Element of D * holds f . (a,b) = H4(a,b)
from BINOP_1:sch 4();
set G = multMagma(# (D *),f #);
multMagma(# (D *),f #) is constituted-FinSeqs
;
then reconsider G = multMagma(# (D *),f #) as non empty strict constituted-FinSeqs multMagma ;
( G is unital & G is associative & G is cancelable & G is uniquely-decomposable )
proof
set N =
G;
set f =
H2(
G);
<*> D = {}
;
then reconsider a =
{} as
Element of
G by FINSEQ_1:def 11;
hence
G is
unital
;
( G is associative & G is cancelable & G is uniquely-decomposable )
hence
G is
associative
;
( G is cancelable & G is uniquely-decomposable )
now for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = clet a,
b,
c be
Element of
G;
( ( a * b = a * c or b * a = c * a ) implies b = c )A3:
(
b * a = b ^ a &
c * a = c ^ a )
by A1;
(
a * b = a ^ b &
a * c = a ^ c )
by A1;
hence
( (
a * b = a * c or
b * a = c * a ) implies
b = c )
by A3, FINSEQ_1:33;
verum end;
hence
G is
cancelable
by Th13;
G is uniquely-decomposable
G is
unital
by A2;
hence
H2(
G) is
having_a_unity
;
MONOID_0:def 9,
MONOID_0:def 20 for a, b being Element of the carrier of G st the multF of G . (a,b) = the_unity_wrt the multF of G holds
( a = b & b = the_unity_wrt the multF of G )
let a9,
b be
Element of
G;
( the multF of G . (a9,b) = the_unity_wrt the multF of G implies ( a9 = b & b = the_unity_wrt the multF of G ) )
now for b being Element of G holds
( H2(G) . (a,b) = b & H2(G) . (b,a) = b )let b be
Element of
G;
( H2(G) . (a,b) = b & H2(G) . (b,a) = b )
(
a [*] b = H2(
G)
. (
a,
b) &
b [*] a = H2(
G)
. (
b,
a) )
;
hence
(
H2(
G)
. (
a,
b)
= b &
H2(
G)
. (
b,
a)
= b )
by A2;
verum end;
then A4:
a is_a_unity_wrt H2(
G)
by BINOP_1:3;
assume
H2(
G)
. (
a9,
b)
= the_unity_wrt H2(
G)
;
( a9 = b & b = the_unity_wrt the multF of G )
then A5:
{} =
a9 [*] b
by A4, BINOP_1:def 8
.=
a9 ^ b
by A1
;
then
a = b
;
hence
(
a9 = b &
b = the_unity_wrt the
multF of
G )
by A4, A5, BINOP_1:def 8;
verum
end;
then reconsider G = G as non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma ;
take
G
; ( the carrier of G = D * & ( for p, q being Element of G holds p [*] q = p ^ q ) )
thus
( the carrier of G = D * & ( for p, q being Element of G holds p [*] q = p ^ q ) )
by A1; verum