let F be FinSequence of COMPLEX ; :: thesis: ( len F >= 1 implies Sum (F *') = (Sum F) *' )
assume len F >= 1 ; :: thesis: Sum (F *') = (Sum F) *'
then len (F *') >= 1 by COMPLSP2:def 1;
hence Sum (F *') = (Sum F) *' by Th20; :: thesis: verum