let A be set ; :: thesis: for b, b1, b2 being Rbag of A st b = b1 + b2 holds
Sum b = (Sum b1) + (Sum b2)
let b, b1, b2 be Rbag of A; :: thesis: ( b = b1 + b2 implies Sum b = (Sum b1) + (Sum b2) )
set S = support b;
set SS = (support b1) \/ (support b2);
A1: dom b2 = A by PARTFUN1:def 2;
then A2: support b2 c= A by PRE_POLY:37;
A3: dom b1 = A by PARTFUN1:def 2;
then support b1 c= A by PRE_POLY:37;
then reconsider SS = (support b1) \/ (support b2) as finite Subset of A by A2, XBOOLE_1:8;
set cS = canFS SS;
consider f1r being FinSequence of REAL such that
A4: f1r = b1 * (canFS SS) and
A5: Sum b1 = Sum f1r by Th11, XBOOLE_1:7;
A6: rng (canFS SS) = SS by FUNCT_2:def 3;
then A7: dom f1r = dom (canFS SS) by A3, A4, RELAT_1:27;
assume A8: b = b1 + b2 ; :: thesis: Sum b = (Sum b1) + (Sum b2)
then support b c= SS by PRE_POLY:75;
then consider f being FinSequence of REAL such that
A9: f = b * (canFS SS) and
A10: Sum b = Sum f by Th11;
dom b = A by PARTFUN1:def 2;
then A11: dom f = dom (canFS SS) by A9, A6, RELAT_1:27;
then A12: len f1r = len f by A7, FINSEQ_3:29;
consider f2r being FinSequence of REAL such that
A13: f2r = b2 * (canFS SS) and
A14: Sum b2 = Sum f2r by Th11, XBOOLE_1:7;
A15: dom f2r = dom (canFS SS) by A1, A13, A6, RELAT_1:27;

A16: now :: thesis: for k being Element of NAT st k in dom f1r holds
f . k = (f1r /. k) + (f2r /. k)

let k be Element of NAT ; :: thesis: ( k in dom f1r implies f . k = (f1r /. k) + (f2r /. k) )
assume A17: k in dom f1r ; :: thesis: f . k = (f1r /. k) + (f2r /. k)
A18: f1r /. k = f1r . k by A17, PARTFUN1:def 6
.= b1 . ((canFS SS) . k) by A4, A17, FUNCT_1:12 ;
A19: f . k = b . ((canFS SS) . k) by A9, A11, A7, A17, FUNCT_1:12;
f2r /. k = f2r . k by A7, A15, A17, PARTFUN1:def 6
.= b2 . ((canFS SS) . k) by A13, A7, A15, A17, FUNCT_1:12 ;
hence f . k = (f1r /. k) + (f2r /. k) by A8, A18, A19, PRE_POLY:def 5; :: thesis: verum

end;

len f1r = len f2r by A7, A15, FINSEQ_3:29;
hence Sum b = (Sum b1) + (Sum b2) by A10, A5, A14, A12, A16, INTEGRA1:21; :: thesis: verum