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 consider f1 being FinSequence of REAL such that
A1: ( Sum b1 = Sum f1 & f1 = b2 * (canFS (support b2)) ) by UPROOTS:def 3;
consider f2 being FinSequence of REAL such that
A2: ( Sum b2 = Sum f2 & f2 = b2 * (canFS (support b2)) ) by UPROOTS:def 3;
thus Sum b1 = Sum b2 by A1, A2; :: thesis: verum