theorem Th2: :: PRE_POLY:2
for D being set holds FlattenSeq (<*> (D *)) = <*> D