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:37;
then A2: F = N * <*n*> by BAGORDER:3
.= N * (canFS (support N)) by A1, UPROOTS:6 ;
Sum F = N . n by FINSOP_1:12;
hence Sum N = N . n by A2, UPROOTS:def 3; :: thesis: verum