let D be non empty set ; :: thesis: for x, y being FinSequence of D holds (D -concatenation) . (x,y) = x ^ y
let x, y be FinSequence of D; :: thesis: (D -concatenation) . (x,y) = x ^ y
reconsider x2 = x, y2 = y as Element of D * by FINSEQ_1:def 11;
reconsider x1 = x2, y1 = y2 as Element of (D *+^) by MONOID_0:def 34;
A1: D -concatenation = the multF of (D *+^) by MONOID_0:def 36;
x1 ^ y1 = x1 * y1 by MONOID_0:def 34
.= (D -concatenation) . (x1,y1) by A1, ALGSTR_0:def 18 ;
hence (D -concatenation) . (x,y) = x ^ y ; :: thesis: verum