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;

hence Sum b = (Sum b1) + (Sum b2) by A10, A5, A14, A12, A16, INTEGRA1:21; :: thesis: verum

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)

len f1r = len f2r
by A7, A15, FINSEQ_3:29;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;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

hence Sum b = (Sum b1) + (Sum b2) by A10, A5, A14, A12, A16, INTEGRA1:21; :: thesis: verum