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 Def14;
hence FlattenSeq <*d*> = d by FINSOP_1:12; :: thesis: verum