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 y2 = F2 as Element of (len F2) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x2 = F1 as Element of (len F1) -tuples_on COMPLEX by FINSEQ_2:92;
Sum (F1 - F2) = addcomplex $$ (diffcomplex .: (F1,F2)) by SEQ_4:def 7
.= diffcomplex . ((addcomplex $$ x2),(addcomplex $$ y2)) by A1, SEQ_4:51, SEQ_4:52, SEQ_4:def 3, SETWOP_2:37
.= (Sum F1) - (Sum F2) by BINOP_2:def 4 ;
hence Sum (F1 - F2) = (Sum F1) - (Sum F2) ; :: thesis: verum