let D be set ; :: thesis: FlattenSeq (<%> (D ^omega )) = <%> D
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 (<%> (D ^omega )) = g "**" (<%> (D ^omega )) by Def14;
A3: {} is Element of D ^omega by AFINSQ_1:47;
reconsider p = {} as Element of D ^omega by AFINSQ_1:47;

now

let a be Element of D ^omega ; :: thesis: ( g . {} ,a = a & g . a,{} = a )
thus g . {} ,a = {} ^ a by A1, A3
.= a by AFINSQ_1:32 ; :: thesis: g . a,{} = a
thus g . a,{} = a ^ {} by A1, A3
.= a by AFINSQ_1:32 ; :: thesis: verum

end;

then A4: p is_a_unity_wrt g by BINOP_1:11;
then g is having_a_unity by SETWISEO:def 2;
then g "**" (<%> (D ^omega )) = the_unity_wrt g by Th84;
hence FlattenSeq (<%> (D ^omega )) = <%> D by A2, A4, BINOP_1:def 8; :: thesis: verum