theorem :: PRE_POLY:5

for D being set
for p, q, r being Element of D * holds FlattenSeq <*p,q,r*> = (p ^ q) ^ r