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 ;
set cS = canFS SS;
consider f1r being FinSequence of REAL such that
A4: f1r = b1 * (canFS SS) and
A5: Sum b1 = Sum f1r by ;
A6: rng (canFS SS) = SS by FUNCT_2:def 3;
then A7: dom f1r = dom (canFS SS) by ;
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 ;
then A12: len f1r = len f by ;
consider f2r being FinSequence of REAL such that
A13: f2r = b2 * (canFS SS) and
A14: Sum b2 = Sum f2r by ;
A15: dom f2r = dom (canFS SS) by ;
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
.= b1 . ((canFS SS) . k) by ;
A19: f . k = b . ((canFS SS) . k) by ;
f2r /. k = f2r . k by
.= b2 . ((canFS SS) . k) by ;
hence f . k = (f1r /. k) + (f2r /. k) by ; :: thesis: verum
end;
len f1r = len f2r by ;
hence Sum b = (Sum b1) + (Sum b2) by ; :: thesis: verum