let F1, F2 be FinSequence of COMPLEX ; :: thesis: ( len F1 = len F2 implies Sum (F1 - F2) = (Sum F1) - (Sum F2) )
assume A1: len F1 = len F2 ; :: thesis: Sum (F1 - F2) = (Sum F1) - (Sum F2)
reconsider x2 = F1 as Element of (len F1) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y2 = F2 as Element of (len F2) -tuples_on COMPLEX by FINSEQ_2:110;
Sum (F1 - F2) = addcomplex $$ (diffcomplex .: F1,F2) by COMPLSP1:def 8
.= diffcomplex . (addcomplex $$ x2),(addcomplex $$ y2) by A1, COMPLSP1:7, COMPLSP1:8, COMPLSP1:def 3, SETWOP_2:48
.= (Sum F1) - (Sum F2) by BINOP_2:def 4 ;
hence Sum (F1 - F2) = (Sum F1) - (Sum F2) ; :: thesis: verum