let A be set ; :: thesis: for b1, b2 being Rbag of A st ( for x being set st x in A holds
b1 . x = b2 . x ) holds
Sum b1 = Sum b2
let b1, b2 be Rbag of A; :: thesis: ( ( for x being set st x in A holds
b1 . x = b2 . x ) implies Sum b1 = Sum b2 )
assume A1: for x being set st x in A holds
b1 . x = b2 . x ; :: thesis: Sum b1 = Sum b2
then for x being set st x in A holds
b2 . x <= b1 . x ;
then A2: Sum b2 <= Sum b1 by Th5;
for x being set st x in A holds
b1 . x <= b2 . x by A1;
then Sum b1 <= Sum b2 by Th5;
hence Sum b1 = Sum b2 by A2, XXREAL_0:1; :: thesis: verum