let f be complex-valued FinSequence; :: thesis: f is Element of COMPLEX (len f)
f is FinSequence of COMPLEX by Lm2;
then f is Element of COMPLEX * by FINSEQ_1:def 11;
then f in { s where s is Element of COMPLEX * : len s = len f } ;
then f in (len f) -tuples_on COMPLEX by FINSEQ_2:def 4;
hence f is Element of COMPLEX (len f) by SEQ_4:def 11; :: thesis: verum