let D be set ; :: thesis: for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
let F, G be FinSequence of D * ; :: thesis: FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
consider g being BinOp of (D * ) such that
A1: for d1, d2 being Element of D * holds g . d1,d2 = d1 ^ d2 and
A2: FlattenSeq (F ^ G) = g "**" (F ^ G) by Def14;

now

let a, b, c be Element of D * ; :: thesis: g . a,(g . b,c) = g . (g . a,b),c
thus g . a,(g . b,c) = a ^ (g . b,c) by A1
.= a ^ (b ^ c) by A1
.= (a ^ b) ^ c by FINSEQ_1:45
.= (g . a,b) ^ c by A1
.= g . (g . a,b),c by A1 ; :: thesis: verum

end;

then A3: g is associative by BINOP_1:def 3;
A4: {} is Element of D * by FINSEQ_1:66;
reconsider p = {} as Element of D * by FINSEQ_1:66;

now

let a be Element of D * ; :: thesis: ( g . {} ,a = a & g . a,{} = a )
thus g . {} ,a = {} ^ a by A1, A4
.= a by FINSEQ_1:47 ; :: thesis: g . a,{} = a
thus g . a,{} = a ^ {} by A1, A4
.= a by FINSEQ_1:47 ; :: thesis: verum

end;

then p is_a_unity_wrt g by BINOP_1:11;
then ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) by SETWISEO:def 2;
hence FlattenSeq (F ^ G) = g . (g "**" F),(g "**" G) by A2, A3, FINSOP_1:6
.= (g "**" F) ^ (g "**" G) by A1
.= (FlattenSeq F) ^ (g "**" G) by A1, Def14
.= (FlattenSeq F) ^ (FlattenSeq G) by A1, Def14 ;
:: thesis: verum