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 Def10;
A3: {} 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, A3
.= a ; :: thesis: g . (a,{}) = a
thus g . (a,{}) = a ^ {} by A1, A3
.= a ; :: thesis: verum

end;

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