theorem Th3: :: PRE_POLY:3

for D being set
for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)