let D be set ; :: thesis: for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
let F, G be XFinSequence of D ^omega ; :: thesis: FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
consider g being BinOp of (D ^omega) such that
A1: for d1, d2 being Element of D ^omega holds g . (d1,d2) = d1 ^ d2 and
A2: FlattenSeq (F ^ G) = g "**" (F ^ G) by Def10;
now :: thesis: for a, b, c being Element of D ^omega holds g . (a,(g . (b,c))) = g . ((g . (a,b)),c)
let a, b, c be Element of D ^omega ; :: 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 AFINSQ_1:27
.= (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 ^omega by AFINSQ_1:43;
reconsider p = {} as Element of D ^omega by AFINSQ_1:43;
now :: thesis: for a being Element of D ^omega holds
( g . ({},a) = a & g . (a,{}) = a )
let a be Element of D ^omega ; :: thesis: ( g . ({},a) = a & g . (a,{}) = a )
thus g . ({},a) = {} ^ a by A1, A4
.= a ; :: thesis: g . (a,{}) = a
thus g . (a,{}) = a ^ {} by A1, A4
.= a ; :: thesis: verum
end;
then p is_a_unity_wrt g by BINOP_1:3;
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, Th41
.= (g "**" F) ^ (g "**" G) by A1
.= (FlattenSeq F) ^ (g "**" G) by A1, Def10
.= (FlattenSeq F) ^ (FlattenSeq G) by A1, Def10 ;
:: thesis: verum