let X, x be set ; :: thesis: for b being Rbag of st dom b = {x} holds
Sum b = b . x
let b be Rbag of ; :: thesis: ( dom b = {x} implies Sum b = b . x )
assume A1: dom b = {x} ; :: thesis: Sum b = b . x
then A2: support b c= {x} by POLYNOM1:41;
{x} c= X by A1, PARTFUN1:def 4;
then consider f being FinSequence of REAL such that
A3: ( f = b * (canFS {x}) & Sum b = Sum f ) by A2, UPROOTS:16;
A4: f = b * <*x*> by A3, UPROOTS:6;
x in dom b by A1, TARSKI:def 1;
then f = <*(b . x)*> by A4, BAGORDER:3;
hence Sum b = b . x by A3, FINSOP_1:12; :: thesis: verum