let X, x be set ; :: thesis: for b being Rbag of X

for y being Real st b = (EmptyBag X) +* (x .--> y) holds

Sum b = y

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

Sum b = y

let y be Real; :: thesis: ( b = (EmptyBag X) +* (x .--> y) implies Sum b = y )

assume A1: b = (EmptyBag X) +* (x .--> y) ; :: thesis: Sum b = y

( dom (x .--> y) = {x} & dom b = (dom (EmptyBag X)) \/ (dom (x .--> y)) ) by A1, FUNCT_4:def 1;

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

A4: f = b * (canFS S) 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 A2, PARTFUN1:def 2;

then x in X by ZFMISC_1:31;

then ( canFS S = <*x*> & x in dom b ) by FINSEQ_1:94, PARTFUN1:def 2;

then f = <*bx*> by A4, FINSEQ_2:34;

hence Sum b = b . x by A5, FINSOP_1:11

.= y by A1, FUNCT_7:94 ;

:: thesis: verum

for y being Real st b = (EmptyBag X) +* (x .--> y) holds

Sum b = y

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

Sum b = y

let y be Real; :: thesis: ( b = (EmptyBag X) +* (x .--> y) implies Sum b = y )

assume A1: b = (EmptyBag X) +* (x .--> y) ; :: thesis: Sum b = y

( dom (x .--> y) = {x} & dom b = (dom (EmptyBag X)) \/ (dom (x .--> y)) ) by A1, FUNCT_4:def 1;

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

then consider f being FinSequence of REAL such that
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 = (EmptyBag X) . a by A1, FUNCT_4:83;

hence contradiction by A3, PBOOLE:5; :: thesis: verum

end;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 = (EmptyBag X) . a by A1, FUNCT_4:83;

hence contradiction by A3, PBOOLE:5; :: thesis: verum

A4: f = b * (canFS S) 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 A2, PARTFUN1:def 2;

then x in X by ZFMISC_1:31;

then ( canFS S = <*x*> & x in dom b ) by FINSEQ_1:94, PARTFUN1:def 2;

then f = <*bx*> by A4, FINSEQ_2:34;

hence Sum b = b . x by A5, FINSOP_1:11

.= y by A1, FUNCT_7:94 ;

:: thesis: verum