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
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;
A11: now :: thesis: for j being Nat st j in Seg (len f1) holds
f1 . j <= f2 . j
let j be Nat; :: thesis: ( j in Seg (len f1) implies f1 . j <= f2 . j )
assume j in Seg (len f1) ; :: thesis: f1 . j <= f2 . j
then A12: j in dom f1 by FINSEQ_1:def 3;
then A13: (canFS S) . j in S by A9, A10, FUNCT_1:3;
( f1 . j = b1 . ((canFS S) . j) & f2 . j = b2 . ((canFS S) . j) ) by A5, A7, A10, A12, FUNCT_1:13;
hence f1 . j <= f2 . j by A1, A13; :: thesis: verum
end;
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; :: thesis: verum