let I be set ; :: thesis: for b being bag of I holds Sum <*b*> = b
let b be bag of I; :: thesis: Sum <*b*> = b
thus Sum <*b*> = Sum ((<*> (Bags I)) ^ <*b*>) by FINSEQ_1:34
.= (Sum (<*> (Bags I))) + b by Th22
.= (EmptyBag I) + b by Th21
.= b by PRE_POLY:53 ; :: thesis: verum