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

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