let n be Nat; :: thesis: for N being Rbag of NAT st support N = {n} holds
Sum N = N . n
let N be Rbag of NAT ; :: thesis: ( support N = {n} implies Sum N = N . n )
reconsider Nn = N . n as Element of REAL by XREAL_0:def 1;
reconsider F = <*Nn*> as FinSequence of REAL ;
assume A1: support N = {n} ; :: thesis: Sum N = N . n
{n} c= dom N by PRE_POLY:37, A1;
then n in dom N by ZFMISC_1:31;
then A2: F = N * <*n*> by FINSEQ_2:34
.= N * (canFS (support N)) by A1, FINSEQ_1:94 ;
Sum F = N . n by FINSOP_1:11;
hence Sum N = N . n by A2, UPROOTS:def 3; :: thesis: verum