let D be set ; :: thesis: FlattenSeq (<*> (D *)) = <*> D
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 (<*> (D *)) = g "**" (<*> (D *)) by Def14;
A3: {} 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, A3
.= a by FINSEQ_1:47 ; :: thesis: g . (a,{}) = a
thus g . (a,{}) = a ^ {} by A1, A3
.= a by FINSEQ_1:47 ; :: 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 *)) = the_unity_wrt g by FINSOP_1:11;
hence FlattenSeq (<*> (D *)) = <*> D by A2, A4, BINOP_1:def 8; :: thesis: verum