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