let I be set ; :: thesis: for b being bag of I
for p being Bags I -valued FinSequence st b in rng p holds
b divides Sum p
let b be bag of I; :: thesis: for p being Bags I -valued FinSequence st b in rng p holds
b divides Sum p
let p be Bags I -valued FinSequence; :: thesis: ( b in rng p implies b divides Sum p )
assume b in rng p ; :: thesis: b divides Sum p
then consider q, r being FinSequence such that
A1: p = (q ^ <*b*>) ^ r by Lem9;
reconsider qb = q ^ <*b*>, r = r as Bags I -valued FinSequence by A1, Lem8;
qb = qb ;
then reconsider q = q as Bags I -valued FinSequence by Lem8;
( Sum p = (Sum (q ^ <*b*>)) + (Sum r) & (Sum (q ^ <*b*>)) + (Sum r) = ((Sum q) + b) + (Sum r) & ((Sum q) + b) + (Sum r) = ((Sum r) + (Sum q)) + b ) by A1, Th22, Th24, RFUNCT_1:8;
hence b divides Sum p by PRE_POLY:50; :: thesis: verum