let D be set ; :: thesis: for d being Element of D * holds FlattenSeq <*d*> = d
let d be Element of D * ; :: thesis: FlattenSeq <*d*> = d
ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & FlattenSeq <*d*> = g "**" <*d*> ) by Def1;
hence FlattenSeq <*d*> = d by FINSOP_1:11; :: thesis: verum