let k be Integer; :: thesis: for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)
let p be FinSequence of INT ; :: thesis: Sum (<*k*> ^ p) = k + (Sum p)
reconsider k = k as Element of INT by INT_1:def 2;
Sum (<*k*> ^ p) = (Sum p) + (Sum <*k*>) by RVSUM_1:75
.= Sum (p ^ <*k*>) by RVSUM_1:75
.= k + (Sum p) by RVSUM_1:74 ;
hence Sum (<*k*> ^ p) = k + (Sum p) ; :: thesis: verum