let f be complex-valued FinSequence; :: thesis: Sum <*f*> = <*(Sum f)*>
A1: ( len <*f*> = 1 & dom <*f*> = dom (Sum <*f*>) & dom <*f*> = Seg 1 ) by Def8, FINSEQ_1:39, FINSEQ_1:38;
A2: (Sum <*f*>) . 1 = Sum (<*f*> . 1) by Def8;
thus Sum <*f*> = <*(Sum f)*> by A1, FINSEQ_3:29, A2, FINSEQ_1:40; :: thesis: verum