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