let D be set ; :: thesis: for p, q being Element of D ^omega holds FlattenSeq <%p,q%> = p ^ q
let p, q be Element of D ^omega ; :: thesis: FlattenSeq <%p,q%> = p ^ q
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 <%p,q%> = g "**" <%p,q%> by Def10;
thus FlattenSeq <%p,q%> = g . (p,q) by A2, Th38
.= p ^ q by A1 ; :: thesis: verum