:: deftheorem Def2 defines Sum UPROOTS:def 3 :
for A being set
for b being Rbag of A
for b₃ being Real holds
( b₃ = Sum b iff ex f being FinSequence of REAL st
( b₃ = Sum f & f = b * (canFS (support b)) ) );