let X, x be set ; :: thesis: for b1, b2 being Rbag of
for y being real number st b2 = b1 +* (x .--> y) holds
Sum b2 = ((Sum b1) + y) - (b1 . x)
let b1, b2 be Rbag of ; :: thesis: for y being real number st b2 = b1 +* (x .--> y) holds
Sum b2 = ((Sum b1) + y) - (b1 . x)
let y be real number ; :: 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)
A2: dom (x .--> y) = {x} by FUNCOP_1:19;
dom b2 = (dom b1) \/ (dom (x .--> y)) by A1, FUNCT_4:def 1;
then {x} c= dom b2 by A2, XBOOLE_1:7;
then {x} c= X by PARTFUN1:def 4;
then A3: x in X by ZFMISC_1:37;
set a = b1 +* (x .--> 0 );
A4a: support (b1 +* (x .--> 0 )) c= (support b1) \/ {x} by Th2;
dom (b1 +* (x .--> 0 )) = (dom b1) \/ (dom (x .--> 0 )) by FUNCT_4:def 1
.= X \/ (dom (x .--> 0 )) by PARTFUN1:def 4
.= X \/ {x} by FUNCOP_1:19
.= X by A3, ZFMISC_1:46 ;
then reconsider a = b1 +* (x .--> 0 ) as Rbag of by A4a, PARTFUN1:def 4, POLYNOM1:def 8, RELAT_1:def 18;
set b = (EmptyBag X) +* (x .--> (b1 . x));
A5a: support ((EmptyBag X) +* (x .--> (b1 . x))) c= (support (EmptyBag X)) \/ {x} by Th2;
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 4
.= X \/ {x} by FUNCOP_1:19
.= X by A3, ZFMISC_1:46 ;
then reconsider b = (EmptyBag X) +* (x .--> (b1 . x)) as Rbag of by A5a, PARTFUN1:def 4, POLYNOM1:def 8, RELAT_1:def 18;
set c = (EmptyBag X) +* (x .--> y);
A6a: support ((EmptyBag X) +* (x .--> y)) c= (support (EmptyBag X)) \/ {x} by Th2;
dom ((EmptyBag X) +* (x .--> y)) = (dom (EmptyBag X)) \/ (dom (x .--> y)) by FUNCT_4:def 1
.= X \/ (dom (x .--> y)) by PARTFUN1:def 4
.= X \/ {x} by FUNCOP_1:19
.= X by A3, ZFMISC_1:46 ;
then reconsider c = (EmptyBag X) +* (x .--> y) as Rbag of by A6a, PARTFUN1:def 4, POLYNOM1:def 8, RELAT_1:def 18;

now

let i be set ; :: thesis: ( i in X implies (a + b) . b₁ = b1 . b₁ )
assume i in X ; :: thesis: (a + b) . b₁ = b1 . b₁
A7: (EmptyBag X) . i = 0 by POLYNOM1:56;

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

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

thus (a + b) . i = (a . i) + (b . i) by POLYNOM1:def 5
.= 0 + (b . i) by A8, FUNCT_7:96
.= b1 . i by A8, FUNCT_7:96 ; :: thesis: verum

end;

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

thus (a + b) . i = (a . i) + (b . i) by POLYNOM1:def 5
.= (b1 . i) + (b . i) by A9, FUNCT_4:88
.= (b1 . i) + 0 by A7, A9, FUNCT_4:88
.= b1 . i ; :: thesis: verum

end;

end;

end;

then A10: (Sum b1) - (Sum b) = ((Sum a) + (Sum b)) - (Sum b) by PBOOLE:3, UPROOTS:17;
A11: Sum c = y by Th8;
A12: Sum b = b1 . x by Th8;

now

let i be set ; :: thesis: ( i in X implies b2 . b₁ = (a + c) . b₁ )
assume i in X ; :: thesis: b2 . b₁ = (a + c) . b₁
A13: (EmptyBag X) . i = 0 by POLYNOM1:56;

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

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

hence b2 . i = y by A1, FUNCT_7:96
.= 0 + (c . i) by A14, FUNCT_7:96
.= (a . i) + (c . i) by A14, FUNCT_7:96
.= (a + c) . i by POLYNOM1:def 5 ;
:: thesis: verum

end;

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

then A16: c . i = 0 by A13, FUNCT_4:88;
thus b2 . i = b1 . i by A1, A15, FUNCT_4:88
.= (a . i) + (c . i) by A15, A16, FUNCT_4:88
.= (a + c) . i by POLYNOM1:def 5 ; :: thesis: verum

end;

end;

end;

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