let X, x be set ; :: thesis: for b being Rbag of X
for y being Real st b = () +* (x .--> y) holds
Sum b = y

let b be Rbag of X; :: thesis: for y being Real st b = () +* (x .--> y) holds
Sum b = y

let y be Real; :: thesis: ( b = () +* (x .--> y) implies Sum b = y )
assume A1: b = () +* (x .--> y) ; :: thesis: Sum b = y
( dom (x .--> y) = {x} & dom b = (dom ()) \/ (dom (x .--> y)) ) by ;
then A2: {x} c= dom b by XBOOLE_1:7;
then reconsider S = {x} as finite Subset of X by PARTFUN1:def 2;
support b c= S
proof
let a be object ; :: 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 A3: b . a <> 0 by PRE_POLY:def 7;
assume not a in S ; :: thesis: contradiction
then a <> x by TARSKI:def 1;
then b . a = () . a by ;
hence contradiction by A3, PBOOLE:5; :: thesis: verum
end;
then consider f being FinSequence of REAL such that
A4: f = b * () and
A5: Sum b = Sum f by UPROOTS:14;
reconsider bx = b . x as Element of REAL by XREAL_0:def 1;
{x} c= X by ;
then x in X by ZFMISC_1:31;
then ( canFS S = <*x*> & x in dom b ) by ;
then f = <*bx*> by ;
hence Sum b = b . x by
.= y by ;
:: thesis: verum