deffunc H₄( 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 = H₄(a,b) from BINOP_1:sch 4();
set G = multMagma(# (D * ),f #);
multMagma(# (D * ),f #) is constituted-FinSeqs

proof

let x be Element of multMagma(# (D * ),f #); :: according to MONOID_0:def 2 :: thesis: x is FinSequence
x is Element of D * ;
hence x is FinSequence ; :: thesis: verum

end;

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 = H₂(G);
<*> D = {} ;
then reconsider a = {} as Element of G by FINSEQ_1:def 11;

A2: now

let b be Element of G; :: thesis: ( a [*] b = b & b [*] a = b )
thus a [*] b = a ^ b by A1
.= b by FINSEQ_1:47 ; :: thesis: b [*] a = b
thus b [*] a = b ^ a by A1
.= b by FINSEQ_1:47 ; :: thesis: verum

end;

hence G is unital by Th6; :: thesis: ( G is associative & G is cancelable & G is uniquely-decomposable )

now

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:45
.= a ^ q by A1
.= a * (b * c) by A1 ; :: thesis: verum

end;

hence G is associative by Lm2; :: thesis: ( G is cancelable & G is uniquely-decomposable )

now

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:46; :: thesis: verum

end;

hence G is cancelable by Th15; :: thesis: G is uniquely-decomposable
G is unital by A2, Th6;
hence H₂(G) is having_a_unity by Def10; :: 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

let b be Element of G; :: thesis: ( H₂(G) . a,b = b & H₂(G) . b,a = b )
( a [*] b = H₂(G) . a,b & b [*] a = H₂(G) . b,a ) ;
hence ( H₂(G) . a,b = b & H₂(G) . b,a = b ) by A2; :: thesis: verum

end;

then A4: a is_a_unity_wrt H₂(G) by BINOP_1:11;
assume H₂(G) . a9,b = the_unity_wrt H₂(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