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 $$ (addcomplex .: (F1,F2)) by SEQ_4:def 6
.= addcomplex . ((addcomplex $$ x2),(addcomplex $$ y2)) by A1, SETWOP_2:35
.= (Sum F1) + (Sum F2) by BINOP_2:def 3 ;
hence Sum (F1 + F2) = (Sum F1) + (Sum F2) ; :: thesis: verum