let n be non empty Ordinal; :: thesis: degree (EmptyBag n) = 0
set b = EmptyBag n;
A1: (EmptyBag n) * (canFS (support (EmptyBag n))) = <*> NAT ;
(EmptyBag n) * (canFS (support (EmptyBag n))) = <*> REAL ;
then reconsider f = (EmptyBag n) * (canFS (support (EmptyBag n))) as FinSequence of REAL ;
consider f being FinSequence of NAT such that
A2: ( 0 = Sum f & f = (EmptyBag n) * (canFS (support (EmptyBag n))) ) by RVSUM_1:72, A1;
thus degree (EmptyBag n) = 0 by A2, UPROOTS:def 4; :: thesis: verum