let A be set ; 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; ( ( 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
; Sum b1 <= Sum b2
set S = (support b1) \/ (support b2);
A2:
dom b2 = A
by PARTFUN1:def 2;
then A3:
support b2 c= A
by PRE_POLY:37;
A4:
dom b1 = A
by PARTFUN1:def 2;
then
support b1 c= A
by PRE_POLY:37;
then reconsider S = (support b1) \/ (support b2) as finite Subset of A by A3, XBOOLE_1:8;
consider f1 being FinSequence of REAL such that
A5:
f1 = b1 * (canFS S)
and
A6:
Sum b1 = Sum f1
by UPROOTS:14, XBOOLE_1:7;
consider f2 being FinSequence of REAL such that
A7:
f2 = b2 * (canFS S)
and
A8:
Sum b2 = Sum f2
by UPROOTS:14, XBOOLE_1:7;
A9:
rng (canFS S) = S
by FUNCT_2:def 3;
then A10:
dom f1 = dom (canFS S)
by A4, A5, RELAT_1:27;
dom f2 = dom (canFS S)
by A2, A7, A9, RELAT_1:27;
then A14:
len f1 = len f2
by A10, FINSEQ_3:29;
( f1 is Element of (len f1) -tuples_on REAL & f2 is Element of (len f2) -tuples_on REAL )
by FINSEQ_2:92;
hence
Sum b1 <= Sum b2
by A6, A8, A14, A11, RVSUM_1:82; verum