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
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 = (EmptyBag X) . a by A1, FUNCT_4:83;
hence contradiction by A3, PBOOLE:5; :: thesis: verum
end;
then consider f being FinSequence of REAL such that
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