let X, x be set ; :: thesis: for b1, b2 being Rbag of X
for y being Real st b2 = b1 +* (x .--> y) holds
Sum b2 = ((Sum b1) + y) - (b1 . x)
let b1, b2 be Rbag of X; :: thesis: for y being Real st b2 = b1 +* (x .--> y) holds
Sum b2 = ((Sum b1) + y) - (b1 . x)
let y be Real; :: thesis: ( b2 = b1 +* (x .--> y) implies Sum b2 = ((Sum b1) + y) - (b1 . x) )
assume A1: b2 = b1 +* (x .--> y) ; :: thesis: Sum b2 = ((Sum b1) + y) - (b1 . x)
( dom (x .--> y) = {x} & dom b2 = (dom b1) \/ (dom (x .--> y)) ) by A1, FUNCT_4:def 1;
then {x} c= dom b2 by XBOOLE_1:7;
then {x} c= X by PARTFUN1:def 2;
then A2: x in X by ZFMISC_1:31;
set c = (EmptyBag X) +* (x .--> y);
A3: dom ((EmptyBag X) +* (x .--> y)) = (dom (EmptyBag X)) \/ (dom (x .--> y)) by FUNCT_4:def 1
.= X \/ (dom (x .--> y)) by PARTFUN1:def 2
.= X \/ {x}
.= X by A2, ZFMISC_1:40 ;
set a = b1 +* (x .--> 0);
A4: dom (b1 +* (x .--> 0)) = (dom b1) \/ (dom (x .--> 0)) by FUNCT_4:def 1
.= X \/ (dom (x .--> 0)) by PARTFUN1:def 2
.= X \/ {x}
.= X by A2, ZFMISC_1:40 ;
set b = (EmptyBag X) +* (x .--> (b1 . x));
A5: dom ((EmptyBag X) +* (x .--> (b1 . x))) = (dom (EmptyBag X)) \/ (dom (x .--> (b1 . x))) by FUNCT_4:def 1
.= X \/ (dom (x .--> (b1 . x))) by PARTFUN1:def 2
.= X \/ {x}
.= X by A2, ZFMISC_1:40 ;
support ((EmptyBag X) +* (x .--> (b1 . x))) c= (support (EmptyBag X)) \/ {x} by Th2;
then reconsider b = (EmptyBag X) +* (x .--> (b1 . x)) as Rbag of X by A5, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;
support (b1 +* (x .--> 0)) c= (support b1) \/ {x} by Th2;
then reconsider a = b1 +* (x .--> 0) as Rbag of X by A4, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;
support ((EmptyBag X) +* (x .--> y)) c= (support (EmptyBag X)) \/ {x} by Th2;
then reconsider c = (EmptyBag X) +* (x .--> y) as Rbag of X by A3, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

now :: thesis: for i being object st i in X holds
(a + b) . i = b1 . i

let i be object ; :: thesis: ( i in X implies (a + b) . b₁ = b1 . b₁ )
assume i in X ; :: thesis: (a + b) . b₁ = b1 . b₁
A6: (EmptyBag X) . i = 0 by PBOOLE:5;

per cases ( i = x or i <> x ) ;

suppose A7: i = x ; :: thesis: (a + b) . b₁ = b1 . b₁

thus (a + b) . i = (a . i) + (b . i) by PRE_POLY:def 5
.= 0 + (b . i) by A7, FUNCT_7:94
.= b1 . i by A7, FUNCT_7:94 ; :: thesis: verum

end;

suppose A8: i <> x ; :: thesis: (a + b) . b₁ = b1 . b₁

thus (a + b) . i = (a . i) + (b . i) by PRE_POLY:def 5
.= (b1 . i) + (b . i) by A8, FUNCT_4:83
.= (b1 . i) + 0 by A6, A8, FUNCT_4:83
.= b1 . i ; :: thesis: verum

end;

end;

end;

then A9: (Sum b1) - (Sum b) = ((Sum a) + (Sum b)) - (Sum b) by PBOOLE:3, UPROOTS:15;
A10: ( Sum c = y & Sum b = b1 . x ) by Th8;

now :: thesis: for i being object st i in X holds
b2 . i = (a + c) . i

let i be object ; :: thesis: ( i in X implies b2 . b₁ = (a + c) . b₁ )
assume i in X ; :: thesis: b2 . b₁ = (a + c) . b₁
A11: (EmptyBag X) . i = 0 by PBOOLE:5;

per cases ( i = x or i <> x ) ;

suppose A12: i = x ; :: thesis: b2 . b₁ = (a + c) . b₁

hence b2 . i = y by A1, FUNCT_7:94
.= 0 + (c . i) by A12, FUNCT_7:94
.= (a . i) + (c . i) by A12, FUNCT_7:94
.= (a + c) . i by PRE_POLY:def 5 ;
:: thesis: verum

end;

suppose A13: i <> x ; :: thesis: b2 . b₁ = (a + c) . b₁

then A14: c . i = 0 by A11, FUNCT_4:83;
thus b2 . i = b1 . i by A1, A13, FUNCT_4:83
.= (a . i) + (c . i) by A13, A14, FUNCT_4:83
.= (a + c) . i by PRE_POLY:def 5 ; :: thesis: verum

end;

end;

end;

hence Sum b2 = ((Sum b1) - (Sum b)) + (Sum c) by A9, PBOOLE:3, UPROOTS:15
.= ((Sum b1) + y) - (b1 . x) by A10 ;
:: thesis: verum