let c be Complex; :: thesis: for F being complex-valued FinSequence holds Sum (F ^ <*c*>) = (Sum F) + c
let F be complex-valued FinSequence; :: thesis: Sum (F ^ <*c*>) = (Sum F) + c
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider F1 = F as FinSequence of COMPLEX by Lm2;
thus Sum (F ^ <*c*>) = Sum (F1 ^ <*s*>)
.= addcomplex . ((addcomplex $$ F1),s) by FINSOP_1:4
.= (Sum F1) + c by BINOP_2:def 3
.= (Sum F) + c ; :: thesis: verum