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