theorem :: FINSEQ_1:107

for f being complex-valued FinSequence holds f is FinSequence of COMPLEX