let n be natural number ; :: 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 F = <*(N . n)*> as FinSequence of REAL ;
assume A1: support N = {n} ; :: thesis: Sum N = N . n
then {n} c= dom N by PRE_POLY:37;
then n in dom N by ZFMISC_1:31;
then A2: F = N * <*n*> by FINSEQ_2:34
.= N * (canFS (support N)) by A1, UPROOTS:4 ;
Sum F = N . n by FINSOP_1:11;
hence Sum N = N . n by A2, UPROOTS:def 3; :: thesis: verum