let seq, seq1 be Complex_Sequence; :: thesis: ( seq is subsequence of seq1 implies ( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 ) )
assume seq is subsequence of seq1 ; :: thesis: ( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 )
then consider Nseq being increasing sequence of NAT such that
A1: seq = seq1 * Nseq by VALUED_0:def 17;
Re seq = (Re seq1) * Nseq by A1, Th22;
hence Re seq is subsequence of Re seq1 ; :: thesis: Im seq is subsequence of Im seq1
Im seq = (Im seq1) * Nseq by A1, Th22;
hence Im seq is subsequence of Im seq1 ; :: thesis: verum