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 Def1;

now :: thesis: for a, b, c being Element of D * holds g . (a,(g . (b,c))) = g . ((g . (a,b)),c)

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:32
.= (g . (a,b)) ^ c by A1
.= g . ((g . (a,b)),c) by A1 ; :: thesis: verum

end;

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

now :: thesis: for a being Element of D * holds
( g . ({},a) = a & g . (a,{}) = a )

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

end;

then p is_a_unity_wrt g by BINOP_1:3;
hence FlattenSeq (F ^ G) = g . ((g "**" F),(g "**" G)) by A2, A3, FINSOP_1:5, SETWISEO:def 2
.= (g "**" F) ^ (g "**" G) by A1
.= (FlattenSeq F) ^ (g "**" G) by A1, Def1
.= (FlattenSeq F) ^ (FlattenSeq G) by A1, Def1 ;
:: thesis: verum