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