let c be Complex; :: thesis: for F being complex-valued FinSequence holds Sum (<*c*> ^ F) = c + (Sum F)
let F be complex-valued FinSequence; :: thesis: Sum (<*c*> ^ F) = c + (Sum F)
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum (<*c*> ^ F) = (Sum <*s*>) + (Sum F) by Th32
.= c + (Sum F) by FINSOP_1:11 ; :: thesis: verum