let X, x be set ; :: thesis: for b being Rbag of
for y being real number st b = (EmptyBag X) +* (x .--> y) holds
Sum b = y
let b be Rbag of ; :: thesis: for y being real number st b = (EmptyBag X) +* (x .--> y) holds
Sum b = y
let y be real number ; :: thesis: ( b = (EmptyBag X) +* (x .--> y) implies Sum b = y )
assume A1: b = (EmptyBag X) +* (x .--> y) ; :: thesis: Sum b = y
A2: dom (x .--> y) = {x} by FUNCOP_1:19;
dom b = (dom (EmptyBag X)) \/ (dom (x .--> y)) by A1, FUNCT_4:def 1;
then A3: {x} c= dom b by A2, XBOOLE_1:7;
then {x} c= X by PARTFUN1:def 4;
then A4: x in X by ZFMISC_1:37;
reconsider S = {x} as finite Subset of X by A3, PARTFUN1:def 4;
support b c= S

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in support b or a in S )
assume a in support b ; :: thesis: a in S
then A5: b . a <> 0 by POLYNOM1:def 7;
assume not a in S ; :: thesis: contradiction
then a <> x by TARSKI:def 1;
then b . a = (EmptyBag X) . a by A1, FUNCT_4:88;
hence contradiction by A5, POLYNOM1:56; :: thesis: verum

end;

then consider f being FinSequence of REAL such that
A6: f = b * (canFS S) and
A7: Sum b = Sum f by UPROOTS:16;
A8: canFS S = <*x*> by UPROOTS:6;
x in dom b by A4, PARTFUN1:def 4;
then f = <*(b . x)*> by A6, A8, BAGORDER:3;
hence Sum b = b . x by A7, FINSOP_1:12
.= y by A1, FUNCT_7:96 ;
:: thesis: verum