let F be complex-valued FinSequence; :: thesis: mlt ((<*> COMPLEX),F) = <*> COMPLEX
F is FinSequence of COMPLEX by Lm2;
hence mlt ((<*> COMPLEX),F) = <*> COMPLEX by FINSEQ_2:73; :: thesis: verum