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