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)
thus 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 ; :: thesis: verum