let D be set ; :: thesis: for F, G being XFinSequence of D ^omega st F c= G holds
FlattenSeq F c= FlattenSeq G
let F, G be XFinSequence of D ^omega ; :: thesis: ( F c= G implies FlattenSeq F c= FlattenSeq G )
assume F c= G ; :: thesis: FlattenSeq F c= FlattenSeq G
then consider F9 being XFinSequence of D ^omega such that
A1: F ^ F9 = G by Th79;
(FlattenSeq F) ^ (FlattenSeq F9) = FlattenSeq G by A1, Th74;
hence FlattenSeq F c= FlattenSeq G by AFINSQ_1:74; :: thesis: verum