theorem Th74: :: AFINSQ_2:75

for D being set
for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)