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