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

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