let A be set ; 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; ( 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
; 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 for k being Element of NAT st k in dom f1r holds
f . k = (f1r /. k) + (f2r /. k)let k be
Element of
NAT ;
( k in dom f1r implies f . k = (f1r /. k) + (f2r /. k) )assume A17:
k in dom f1r
;
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;
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; verum