for F being complex-valued FinSequence holds F is FinSequence of COMPLEX by Lm5;