let A be set ; :: thesis: for b, b1, b2 being Rbag of st b = b1 + b2 holds
Sum b = (Sum b1) + (Sum b2)
let b, b1, b2 be Rbag of ; :: thesis: ( b = b1 + b2 implies Sum b = (Sum b1) + (Sum b2) )
assume A1: b = b1 + b2 ; :: thesis: Sum b = (Sum b1) + (Sum b2)
set S = support b;
set SS = (support b1) \/ (support b2);
A2: ( dom b = A & dom b1 = A & dom b2 = A ) by PARTFUN1:def 4;
then ( support b1 c= A & support b2 c= A ) by POLYNOM1:41;
then reconsider SS = (support b1) \/ (support b2) as finite Subset of A by XBOOLE_1:8;
support b c= SS by A1, POLYNOM1:91;
then consider f being FinSequence of REAL such that
A3: f = b * (canFS SS) and
A4: Sum b = Sum f by Th16;
consider f1r being FinSequence of REAL such that
A5: f1r = b1 * (canFS SS) and
A6: Sum b1 = Sum f1r by Th16, XBOOLE_1:7;
consider f2r being FinSequence of REAL such that
A7: f2r = b2 * (canFS SS) and
A8: Sum b2 = Sum f2r by Th16, XBOOLE_1:7;
set cS = canFS SS;
rng (canFS SS) = SS by FUNCT_2:def 3;
then A9: ( dom f = dom (canFS SS) & dom f1r = dom (canFS SS) & dom f2r = dom (canFS SS) ) by A2, A3, A5, A7, RELAT_1:46;
then A10: ( len f1r = len f2r & len f1r = len f ) by FINSEQ_3:31;

now

let k be Element of NAT ; :: thesis: ( k in dom f1r implies f . k = (f1r /. k) + (f2r /. k) )
assume A11: k in dom f1r ; :: thesis: f . k = (f1r /. k) + (f2r /. k)
A12: f1r /. k = f1r . k by A11, PARTFUN1:def 8
.= b1 . ((canFS SS) . k) by A5, A11, FUNCT_1:22 ;
A13: f2r /. k = f2r . k by A9, A11, PARTFUN1:def 8
.= b2 . ((canFS SS) . k) by A7, A9, A11, FUNCT_1:22 ;
f . k = b . ((canFS SS) . k) by A3, A9, A11, FUNCT_1:22;
hence f . k = (f1r /. k) + (f2r /. k) by A1, A12, A13, POLYNOM1:def 5; :: thesis: verum

end;

hence Sum b = (Sum b1) + (Sum b2) by A4, A6, A8, A10, INTEGRA1:23; :: thesis: verum