let X, x be set ; :: thesis: for b being Rbag of X st dom b = {x} holds
Sum b = b . x
let b be Rbag of X; :: thesis: ( dom b = {x} implies Sum b = b . x )
assume A1: dom b = {x} ; :: thesis: Sum b = b . x
then A2: x in dom b by TARSKI:def 1;
( support b c= {x} & {x} c= X ) by A1, PRE_POLY:37;
then consider f being FinSequence of REAL such that
A3: f = b * (canFS {x}) and
A4: Sum b = Sum f by UPROOTS:14;
reconsider bx = b . x as Element of REAL by XREAL_0:def 1;
f = b * <*x*> by A3, FINSEQ_1:94;
then f = <*bx*> by A2, FINSEQ_2:34;
hence Sum b = b . x by A4, FINSOP_1:11; :: thesis: verum