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 F9 being FinSequence of D * such that
A1: F ^ F9 = G by FINSEQ_4:82;
(FlattenSeq F) ^ (FlattenSeq F9) = FlattenSeq G by A1, Th3;
hence FlattenSeq F c= FlattenSeq G by FINSEQ_6:10; :: thesis: verum