let A1, A2 be set ; :: thesis: for b1 being Rbag of A1
for b2 being Rbag of A2 st b1 = b2 holds
Sum b1 = Sum b2
let b1 be Rbag of A1; :: thesis: for b2 being Rbag of A2 st b1 = b2 holds
Sum b1 = Sum b2
let b2 be Rbag of A2; :: thesis: ( b1 = b2 implies Sum b1 = Sum b2 )
assume b1 = b2 ; :: thesis: Sum b1 = Sum b2
then ex f1 being FinSequence of REAL st
( Sum b1 = Sum f1 & f1 = b2 * (canFS (support b2)) ) by UPROOTS:def 3;
hence Sum b1 = Sum b2 by UPROOTS:def 3; :: thesis: verum