theorem Th1: :: PRE_POLY:1

for D being set
for d being Element of D * holds FlattenSeq <*d*> = d