let I be set ; :: thesis: for b being bag of I
for p being Bags I -valued FinSequence holds Sum (<*b*> ^ p) = b + (Sum p)
let b be bag of I; :: thesis: for p being Bags I -valued FinSequence holds Sum (<*b*> ^ p) = b + (Sum p)
let p be Bags I -valued FinSequence; :: thesis: Sum (<*b*> ^ p) = b + (Sum p)
thus Sum (<*b*> ^ p) = (Sum <*b*>) + (Sum p) by Th24
.= b + (Sum p) by Th23 ; :: thesis: verum