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