let D be set ; for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
let F, G be FinSequence of D * ; 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 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 * ;
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
;
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;
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
;
verum