let f be FinSequence of COMPLEX ; :: thesis: f is Element of COMPLEX (len f)
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 COMPLSP1:def 12; :: thesis: verum