let D be non empty set ; :: thesis: for f, g being FinSequence of D * holds (D -concatenation) "**" (f ^ g) = ((D -concatenation) "**" f) ^ ((D -concatenation) "**" g)
let f, g be FinSequence of D * ; :: thesis: (D -concatenation) "**" (f ^ g) = ((D -concatenation) "**" f) ^ ((D -concatenation) "**" g)
set DC = D -concatenation ;
reconsider df = (D -concatenation) "**" f, dg = (D -concatenation) "**" g as Element of (D *+^) by MONOID_0:def 34;
thus (D -concatenation) "**" (f ^ g) = (D -concatenation) . (((D -concatenation) "**" f),((D -concatenation) "**" g)) by MONOID_0:67, FINSOP_1:5
.= the multF of (D *+^) . (((D -concatenation) "**" f),((D -concatenation) "**" g)) by MONOID_0:def 36
.= df * dg by ALGSTR_0:def 18
.= ((D -concatenation) "**" f) ^ ((D -concatenation) "**" g) by MONOID_0:def 34 ; :: thesis: verum