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 Def1;
A3: {} is Element of D * by FINSEQ_1:49;
reconsider p = {} as Element of D * by FINSEQ_1:49;
now :: thesis: for a being Element of D * holds
( g . ({},a) = a & g . (a,{}) = a )
let a be Element of D * ; :: thesis: ( g . ({},a) = a & g . (a,{}) = a )
thus g . ({},a) = {} ^ a by A1, A3
.= a by FINSEQ_1:34 ; :: thesis: g . (a,{}) = a
thus g . (a,{}) = a ^ {} by A1, A3
.= a by FINSEQ_1:34 ; :: thesis: verum
end;
then A4: p is_a_unity_wrt g by BINOP_1:3;
then g "**" (<*> (D *)) = the_unity_wrt g by FINSOP_1:10, SETWISEO:def 2;
hence FlattenSeq (<*> (D *)) = <*> D by A2, A4, BINOP_1:def 8; :: thesis: verum