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;
A2: now :: thesis: for b being Element of G holds
( a [*] b = b & b [*] a = b )
let b be Element of G; :: thesis: ( a [*] b = b & b [*] a = b )
thus a [*] b = a ^ b by A1
.= b by FINSEQ_1:34 ; :: thesis: b [*] a = b
thus b [*] a = b ^ a by A1
.= b by FINSEQ_1:34 ; :: thesis: verum
end;
hence G is unital ; :: thesis: ( G is associative & G is cancelable & G is uniquely-decomposable )
now :: thesis: for a, b, c being Element of G holds (a * b) * c = a * (b * c)
let a, b, c be Element of G; :: thesis: (a * b) * c = a * (b * c)
reconsider p = a [*] b, q = b [*] c as Element of G ;
thus (a * b) * c = p ^ c by A1
.= (a ^ b) ^ c by A1
.= a ^ (b ^ c) by FINSEQ_1:32
.= a ^ q by A1
.= a * (b * c) by A1 ; :: thesis: verum
end;
hence G is associative ; :: thesis: ( G is cancelable & G is uniquely-decomposable )
now :: thesis: for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c
let a, b, c be Element of G; :: thesis: ( ( 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; :: thesis: verum
end;
hence G is cancelable by Th13; :: thesis: G is uniquely-decomposable
G is unital by A2;
hence H2(G) is having_a_unity ; :: according to MONOID_0:def 9,MONOID_0:def 20 :: thesis: 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; :: thesis: ( 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 :: thesis: for b being Element of G holds
( H2(G) . (a,b) = b & H2(G) . (b,a) = b )
let b be Element of G; :: thesis: ( 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; :: thesis: 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) ; :: thesis: ( 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; :: thesis: verum
end;
then reconsider G = G as non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma ;
take G ; :: thesis: ( 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; :: thesis: verum