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