let D be set ; 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 ; 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 Def10;
thus FlattenSeq <%p,q,r%> =
g . ((g . (p,q)),r)
by A2, Th39
.=
(g . (p,q)) ^ r
by A1
.=
(p ^ q) ^ r
by A1
; verum