let n be natural number ; :: thesis: for N being Rbag of st support N = {n} holds
Sum N = N . n
let N be Rbag of ; :: thesis: ( support N = {n} implies Sum N = N . n )
assume A1: support N = {n} ; :: thesis: Sum N = N . n
then {n} c= dom N by POLYNOM1:41;
then A2: n in dom N by ZFMISC_1:37;
reconsider F = <*(N . n)*> as FinSequence of REAL ;
A3: Sum F = N . n by FINSOP_1:12;
F = N * <*n*> by A2, BAGORDER:3
.= N * (canFS (support N)) by A1, UPROOTS:6 ;
hence Sum N = N . n by A3, UPROOTS:def 3; :: thesis: verum