rng x c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence x is FinSequence of COMPLEX by FINSEQ_1:def 4; :: thesis: verum