let D be set ; :: thesis: for F, G being FinSequence of D * st F c= G holds
FlattenSeq F c= FlattenSeq G
let F, G be FinSequence of D * ; :: thesis: ( F c= G implies FlattenSeq F c= FlattenSeq G )
assume F c= G ; :: thesis: FlattenSeq F c= FlattenSeq G
then consider F' being FinSequence of D * such that
A1: F ^ F' = G by FINSEQ_4:97;
(FlattenSeq F) ^ (FlattenSeq F') = FlattenSeq G by A1, Th21;
hence FlattenSeq F c= FlattenSeq G by FINSEQ_6:12; :: thesis: verum