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