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